diff options
| author | Kazuhiko Sakaguchi | 2019-08-30 11:30:21 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-10-30 23:19:33 +0100 |
| commit | d60c67b8f33f55e11ca159246d2a447102f10f20 (patch) | |
| tree | 74fecfdcc5b2429e5cf199f9daa48a56540e2359 /mathcomp/algebra/ssrint.v | |
| parent | c5bd1d4d29021688db59495a8b60c84f5dea6b77 (diff) | |
Change the order of arguments in `ltngtP`
from
`ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)`
to
`ltngtP m n : compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`,
to make it tries to match subterms with `m < n` first, `m <= n`, then `m == n`.
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). |