diff options
| author | Cyril Cohen | 2020-11-23 22:41:17 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-24 02:15:48 +0100 |
| commit | ac30dae7377f9762ceba1c5553f0542831a0bb5c (patch) | |
| tree | 38e78d05317f2de668038a6a3e50647e94a9d043 /mathcomp/ssreflect/path.v | |
| parent | 84d3168ae3436acec2df0b6f83e85ae7c5310ce1 (diff) | |
Using [dup] in path
Diffstat (limited to 'mathcomp/ssreflect/path.v')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 269be3e..5a9de74 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -549,8 +549,8 @@ Lemma sorted_eq_in s1 s2 : {in s1 & &, transitive leT} -> {in s1 &, antisymmetric leT} -> sorted leT s1 -> sorted leT s2 -> perm_eq s1 s2 -> s1 = s2. Proof. -move=> /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_anti ss1 ss2 s1s2. -move: ss1 ss2 (s1s2); have /all_sigP[s1' ->] := allss s1. +move=> /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_anti + + /[dup] s1s2. +have /all_sigP[s1' ->] := allss s1. have /all_sigP[{s1s2}s2 ->] : all (mem s1) s2 by rewrite -(perm_all _ s1s2). by rewrite !sorted_map => ss1' ss2 /(perm_map_inj val_inj)/(sorted_eq leT_tr)->. Qed. @@ -559,7 +559,7 @@ Lemma irr_sorted_eq_in s1 s2 : {in s1 & &, transitive leT} -> {in s1, irreflexive leT} -> sorted leT s1 -> sorted leT s2 -> s1 =i s2 -> s1 = s2. Proof. -move=> /in3_sig leT_tr /in1_sig leT_irr ss1 ss2 s1s2; move: ss1 ss2 (s1s2). +move=> /in3_sig leT_tr /in1_sig leT_irr + + /[dup] s1s2. have /all_sigP[s1' ->] := allss s1. have /all_sigP[s2' ->] : all (mem s1) s2 by rewrite -(eq_all_r s1s2). rewrite !sorted_map => ss1' ss2' {}s1s2; congr map. |