diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/real_closed/polyorder.v | 5 | ||||
| -rw-r--r-- | mathcomp/solvable/abelian.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 31 |
3 files changed, 25 insertions, 13 deletions
diff --git a/mathcomp/real_closed/polyorder.v b/mathcomp/real_closed/polyorder.v index f18ec89..2da4dc9 100644 --- a/mathcomp/real_closed/polyorder.v +++ b/mathcomp/real_closed/polyorder.v @@ -108,10 +108,7 @@ Qed. Lemma muP p x n : p != 0 -> (('X - x%:P)^+n %| p) && ~~(('X - x%:P)^+n.+1 %| p) = (n == \mu_x p). Proof. -move=> hp0; rewrite !root_le_mu//; case: (ltngtP n (\mu_x p))=> hn. -+ by rewrite ltnW//=. -+ by rewrite leqNgt hn. -+ by rewrite hn leqnn. +by move=> hp0; rewrite !root_le_mu//; case: (ltngtP n (\mu_x p)). Qed. Lemma mu_gt0 p x : p != 0 -> (0 < \mu_x p)%N = root p x. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index e608c4f..45168a0 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -1745,7 +1745,7 @@ pose cnt_p k := count [pred x : gT | logn p #[x] > k]. have cnt_b b: \big[dprod/1]_(x <- b) <[x]> = G -> count [pred x | #[x] == p ^ k.+1]%N b = cnt_p k b - cnt_p k.+1 b. - move/p_bG; elim: b => //= _ b IHb /andP[/p_natP[j ->] /IHb-> {IHb}]. - rewrite eqn_leq !leq_exp2l ?prime_gt1 // -eqn_leq pfactorK // leqNgt. + rewrite eqn_leq !leq_exp2l ?prime_gt1 // -eqn_leq pfactorK //. case: ltngtP => // _ {j}; rewrite subSn // add0n; elim: b => //= y b IHb. by rewrite leq_add // ltn_neqAle; case: (~~ _). by rewrite !cnt_b // /cnt_p !(@count_logn_dprod_cycle _ _ _ G). diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 9b9f6a5..0cf70a8 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -441,15 +441,18 @@ CoInductive eqn0_xor_gt0 n : bool -> bool -> Set := Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n). Proof. by case: n; constructor. Qed. -CoInductive compare_nat m n : bool -> bool -> bool -> Set := - | CompareNatLt of m < n : compare_nat m n true false false - | CompareNatGt of m > n : compare_nat m n false true false - | CompareNatEq of m = n : compare_nat m n false false true. +CoInductive compare_nat m n : bool -> bool -> bool -> bool -> bool -> bool -> Set := + | CompareNatLt of m < n : compare_nat m n true false true false false false + | CompareNatGt of m > n : compare_nat m n false true false true false false + | CompareNatEq of m = n : compare_nat m n true true false false true true. -Lemma ltngtP m n : compare_nat m n (m < n) (n < m) (m == n). +Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n). Proof. -rewrite ltn_neqAle eqn_leq; case: ltnP; first by constructor. -by rewrite leq_eqVlt orbC; case: leqP; constructor; first apply/eqnP. +rewrite !ltn_neqAle [_ == m]eq_sym; case: ltnP => [mn|]. + by rewrite ltnW // gtn_eqF //; constructor. +rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_nm eq_mn. + by rewrite ltn_eqF //; constructor. +by rewrite eq_mn; constructor; apply/eqP. Qed. (* Monotonicity lemmas *) @@ -562,7 +565,7 @@ Lemma maxnC : commutative maxn. Proof. by move=> m n; rewrite /maxn; case ltngtP. Qed. Lemma maxnE m n : maxn m n = m + (n - m). -Proof. by rewrite /maxn addnC; case: leqP => [/eqnP-> | /ltnW/subnK]. Qed. +Proof. by rewrite /maxn addnC; case: leqP => [/eqnP->|/ltnW/subnK]. Qed. Lemma maxnAC : right_commutative maxn. Proof. by move=> m n p; rewrite !maxnE -!addnA !subnDA -!maxnE maxnC. Qed. @@ -1591,3 +1594,15 @@ Ltac nat_congr := first apply: (congr1 (addn X1) _); symmetry end ]. + +Module mc_1_6. + +CoInductive compare_nat m n : bool -> bool -> bool -> Set := + | CompareNatLt of m < n : compare_nat m n true false false + | CompareNatGt of m > n : compare_nat m n false true false + | CompareNatEq of m = n : compare_nat m n false false true. + +Lemma ltngtP m n : compare_nat m n (m < n) (n < m) (m == n). +Proof. by case: ltngtP; constructor. Qed. + +End mc_1_6. |