diff options
| author | Cyril Cohen | 2020-09-02 14:17:11 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-08 01:01:57 +0200 |
| commit | 8710f75d73ce4f1c010f1792ebba37a08852c23b (patch) | |
| tree | d58e639b7ca47c522572092aaed51f3e209d5677 /mathcomp/ssreflect/path.v | |
| parent | c43abda6504f909db9884f2c42f764378471129f (diff) | |
split_find_nth and split_find lemmas
Diffstat (limited to 'mathcomp/ssreflect/path.v')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 6e72af0..7d1f0e9 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -193,10 +193,7 @@ Variant split x : seq T -> seq T -> seq T -> Type := Lemma splitP p x (i := index x p) : x \in p -> split x p (take i p) (drop i.+1 p). -Proof. -move=> p_x; have lt_ip: i < size p by rewrite index_mem. -by rewrite -{1}(cat_take_drop i p) (drop_nth x lt_ip) -cat_rcons nth_index. -Qed. +Proof. by rewrite -has_pred1 => /split_find[? ? ? /eqP->]; constructor. Qed. Variant splitl x1 x : seq T -> Type := Splitl p1 p2 of last x1 p1 = x : splitl x1 x (p1 ++ p2). |