diff options
| author | Cyril Cohen | 2020-11-19 18:33:21 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-19 21:38:46 +0100 |
| commit | e565f8d9bebd4fd681c34086d5448dbaebc11976 (patch) | |
| tree | 3e74907bf8e310b6400b7c340357ad44fc44a83f /mathcomp/ssreflect/order.v | |
| parent | 0dbefe01e54a467b7932a514355f0435b4cfb978 (diff) | |
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/ssreflect/order.v')
| -rw-r--r-- | mathcomp/ssreflect/order.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 7cd178d..3cf68d3 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -6968,7 +6968,7 @@ Lemma leEtprod n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= lexx; symmetry; apply/forallP => []. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ <= _]le_cons [t1 <= t2 :> seq _]IHn. apply/idP/forallP => [/andP[lex12 /forallP/= let12 i]|lext12]. by case: (unliftP ord0 i) => [j ->|->]//; rewrite !tnthS. @@ -7278,7 +7278,7 @@ Lemma lexi_tupleP n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= lexx; constructor; exists ord0 => -[]. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ <= _]lexi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: comparableP => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. @@ -7299,7 +7299,7 @@ Lemma ltxi_tupleP n T (t1 t2 : n.-tuple T) : Proof. elim: n => [|n IHn] in t1 t2 *. by rewrite tuple0 [t2]tuple0/= ltxx; constructor => - [] []. -case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2]. +case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2]. rewrite [_ < _]ltxi_cons; apply: (iffP idP) => [|[k leif_xt12]]. case: (comparableP x1 x2) => //= [ltx12 _|-> /IHn[k kP]]. exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->. |