Doc, comments, changelog and better proofs

- adding a doc paragraph on displays
- Changelog
- better proofs for new logn, gcdn, lcmn, partn facts
- Putting comments in the example of nat

1 files changed, 18 insertions, 30 deletions

diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 4f0ee77..d8f5939 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -741,29 +741,6 @@ case: (posnP n) => [-> |]; first by rewrite div0n logn0.
 by rewrite -{1 3}def_n muln_gt0 => /andP[q_gt0 m_gt0]; rewrite lognM ?addnK.
 Qed.
 
-Lemma logn_gcd p m n : 0 < m -> 0 < n ->
-  logn p (gcdn m n) = minn (logn p m) (logn p n).
-Proof.
-case p_pr: (prime p); last by rewrite /logn p_pr.
-wlog le_log_mn: m n / logn p m <= logn p n => [hwlog m_gt0 n_gt0|].
-  have /orP[] := leq_total (logn p m) (logn p n) => /hwlog; first exact.
-  by rewrite gcdnC minnC; apply.
-have xlp := pfactor_coprime p_pr => /xlp[m' cpm' {1}->] /xlp[n' cpn' {1}->].
-rewrite (minn_idPl _)// -(subnK le_log_mn) expnD mulnA -muln_gcdl.
-rewrite lognM//; last first.
-  rewrite Gauss_gcdl ?coprime_expr 1?coprime_sym// gcdn_gt0.
-  by case: m' cpm' p_pr => //; rewrite /coprime gcdn0 => /eqP->.
-rewrite pfactorK// Gauss_gcdl; last by rewrite coprime_expr// coprime_sym.
-by rewrite logn_coprime// /coprime gcdnA (eqP cpm') gcd1n.
-Qed.
-
-Lemma logn_lcm p m n : 0 < m -> 0 < n ->
-  logn p (lcmn m n) = maxn (logn p m) (logn p n).
-Proof.
-move=> m_gt0 n_gt0; rewrite /lcmn logn_div ?dvdn_mull ?dvdn_gcdr//.
-by rewrite lognM// logn_gcd// -addn_min_max addnC addnK.
-Qed.
-
 Lemma dvdn_pfactor p d n : prime p ->
   reflect (exists2 m, m <= n & d = p ^ m) (d %| p ^ n).
 Proof.
@@ -926,10 +903,9 @@ by case: and3P => [[_ n_gt0 p_dv_n]|]; rewrite ?if_same // andbC dvdn_leq.
 Qed.
 
 Lemma eq_partn_from_log m n (pi : nat_pred) : 0 < m -> 0 < n ->
-  (forall p, p \in pi -> logn p m = logn p n) -> m`_pi = n`_pi.
+  {in pi, logn^~ m =1 logn^~ n} -> m`_pi = n`_pi.
 Proof.
-move=> m_gt0 n_gt0 eq_log.
-rewrite !(@widen_partn (maxn m n)) ?leq_max ?leqnn ?orbT//.
+move=> m0 n0 eq_log; rewrite !(@widen_partn (maxn m n)) ?leq_maxl ?leq_maxr//.
 by apply: eq_bigr => p /eq_log ->.
 Qed.
 
@@ -1017,11 +993,9 @@ move=> n_gt0; rewrite -{2}(partn_pi n_gt0) {2}/partn big_mkcond /=.
 by apply: eq_bigr => p _; rewrite -logn_gt0; case: (logn p _).
 Qed.
 
-Lemma eqn_from_log m n : 0 < m -> 0 < n ->
-  (forall p, logn p m = logn p n) -> m = n.
+Lemma eqn_from_log m n : 0 < m -> 0 < n -> logn^~ m =1 logn^~ n -> m = n.
 Proof.
-move=> m_gt0 n_gt0 eq_log; rewrite -[m]partnT// -[n]partnT//.
-exact: eq_partn_from_log.
+by move=> ? ? /(@in1W _ predT)/eq_partn_from_log; rewrite !partnT// => ->.
 Qed.
 
 Lemma partnC pi n : n > 0 -> n`_pi * n`_pi^' = n.
@@ -1089,6 +1063,20 @@ apply/dvdn_biggcdP=> i Pi; rewrite -(partnC pi (F_gt0 i Pi)) dvdn_mul //.
 by rewrite partn_dvd ?F_gt0 // (@biggcdn_inf _ i).
 Qed.
 
+Lemma logn_gcd p m n : 0 < m -> 0 < n ->
+  logn p (gcdn m n) = minn (logn p m) (logn p n).
+Proof.
+move=> m_gt0 n_gt0; case p_pr: (prime p); last by rewrite /logn p_pr.
+by apply: (@expnI p); rewrite ?prime_gt1// expn_min -!p_part partn_gcd.
+Qed.
+
+Lemma logn_lcm p m n : 0 < m -> 0 < n ->
+  logn p (lcmn m n) = maxn (logn p m) (logn p n).
+Proof.
+move=> m_gt0 n_gt0; rewrite /lcmn logn_div ?dvdn_mull ?dvdn_gcdr//.
+by rewrite lognM// logn_gcd// -addn_min_max addnC addnK.
+Qed.
+
 Lemma sub_in_pnat pi rho n :
   {in \pi(n), {subset pi <= rho}} -> pi.-nat n -> rho.-nat n.
 Proof.