diff options
| author | Cyril Cohen | 2019-10-31 19:07:15 +0100 |
|---|---|---|
| committer | GitHub | 2019-10-31 19:07:15 +0100 |
| commit | 71e397e46b65c1c27a65471170d71f388c8a45f1 (patch) | |
| tree | 74fecfdcc5b2429e5cf199f9daa48a56540e2359 /mathcomp/algebra/ssrint.v | |
| parent | c5bd1d4d29021688db59495a8b60c84f5dea6b77 (diff) | |
| parent | d60c67b8f33f55e11ca159246d2a447102f10f20 (diff) | |
Merge pull request #378 from pi8027/fix-ltngtP
Reorder the arguments in `compare_nat` and `ltngtP`
Diffstat (limited to 'mathcomp/algebra/ssrint.v')
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 3c4c002..2a17a4a 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -138,9 +138,9 @@ Lemma oppzK : involutive oppz. Proof. by do 2?case. Qed. Lemma oppz_add : {morph oppz : m n / m + n}. Proof. -move=> [[|n]|n] [[|m]|m] /=; rewrite ?NegzE ?oppzK ?addnS ?addn0 ?subn0 //; - rewrite ?ltnS[m <= n]leqNgt [n <= m]leqNgt; case: ltngtP=> hmn /=; - by rewrite ?hmn ?subnn // ?oppzK ?subSS ?subnS ?prednK // ?subn_gt0. +by move=> [[|n]|n] [[|m]|m] /=; rewrite ?addn0 ?subn0 ?addnS //; + rewrite !NegzE !ltnS !subSS; case: ltngtP => [?|?|->]; + rewrite ?subnn // ?oppzK ?subnS ?prednK // subn_gt0. Qed. Lemma add1Pz (n : int) : 1 + (n - 1) = n. @@ -154,9 +154,9 @@ Qed. Lemma addSnz (m : nat) (n : int) : (m.+1%N) + n = 1 + (m + n). Proof. move: m n=> [|m] [] [|n] //=; rewrite ?add1n ?subn1 // !(ltnS, subSS). -rewrite [n <= m]leqNgt; case: ltngtP=> hmn /=; rewrite ?hmn ?subnn //. +case: ltngtP=> hnm /=; rewrite ?hnm ?subnn //. by rewrite subnS add1n prednK ?subn_gt0. -by rewrite ltnS leqn0 subn_eq0 leqNgt hmn /= subnS subn1. +by rewrite ltnS leqn0 subn_eq0 leqNgt hnm /= subnS subn1. Qed. Lemma addSz (m n : int) : (1 + m) + n = 1 + (m + n). |