diff options
| author | affeldt-aist | 2020-11-20 12:41:11 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 12:41:11 +0900 |
| commit | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (patch) | |
| tree | 076b8d8c53eaaf424258388bbd0068970c55b85f /mathcomp/ssreflect/order.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
| parent | e565f8d9bebd4fd681c34086d5448dbaebc11976 (diff) | |
Merge pull request #658 from CohenCyril/duplicate_clear
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 f40c1d5..97e34a2 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -6965,7 +6965,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. @@ -7275,7 +7275,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)->. @@ -7296,7 +7296,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)->. |