A few more revisions

11 files changed, 38 insertions, 66 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 8a65cf2..e35d2c8 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -949,9 +949,7 @@ Proof. by move=> ge_m_n; rewrite /index_iota (eqnP ge_m_n) big_nil. Qed.
 Lemma big_ltn_cond m n (P : pred nat) F :
     m < n -> let x := \big[op/idx]_(m.+1 <= i < n | P i) F i in
   \big[op/idx]_(m <= i < n | P i) F i = if P m then op (F m) x else x.
-Proof.
-by case: n => [//|n] le_m_n; rewrite /index_iota subSn // big_cons.
-Qed.
+Proof. by case: n => [//|n] le_m_n; rewrite /index_iota subSn // big_cons. Qed.
 
 Lemma big_ltn m n F :
      m < n ->
@@ -1329,7 +1327,7 @@ Lemma perm_big (I : eqType) r1 r2 (P : pred I) F :
 Proof.
 move/permP; rewrite !(big_mkcond _ _ P).
 elim: r1 r2 => [|i r1 IHr1] r2 eq_r12.
-  by case: r2 eq_r12 => // i r2; move/(_ (pred1 i)); rewrite /= eqxx.
+  by case: r2 eq_r12 => // i r2 /(_ (pred1 i)); rewrite /= eqxx.
 have r2i: i \in r2 by rewrite -has_pred1 has_count -eq_r12 /= eqxx.
 case/splitPr: r2 / r2i => [r3 r4] in eq_r12 *; rewrite big_cat /= !big_cons.
 rewrite mulmCA; congr (_ * _); rewrite -big_cat; apply: IHr1 => a.
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 24c2adf..d419745 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -80,8 +80,7 @@ have vFpV i: i != Fp0 -> mFp (vFp i) i = Fp1.
   rewrite coprime_sym prime_coprime //; apply/negP=> /(dvdn_leq i_gt0).
   by rewrite leqNgt ltn_ord.
 have vFp0 i: i != Fp0 -> vFp i != Fp0.
-  move/vFpV=> inv_i; apply/eqP=> vFp0.
-  by have:= congr1 val inv_i; rewrite vFp0 /= mod0n.
+  by move/vFpV; apply/contra_eq_neq => ->; rewrite -val_eqE /= mul0n mod0n.
 have vFpK: {in predC1 Fp0, involutive vFp}.
   move=> i n0i; rewrite /= -[vFp _]mFp1r -(vFpV _ n0i) mFpA.
   by rewrite vFpV (vFp0, mFp1).
@@ -113,7 +112,7 @@ rewrite [mFpM _ _]mFp1 (bigD1 Fpn1) -?mFpA -/mFpM; last first.
   by rewrite [ltv _]ltn_neqAle vFpId eqxx orbT eq_sym eqF1n1.
 rewrite (reindex_onto vFp vFp) -/mFpM => [|i]; last by do 3!case/andP; auto.
 rewrite (eq_bigl (xpredD1 ltv Fp0)) => [|i]; last first.
-  rewrite andbC -!andbA -2!negb_or -vFpId orbC -leq_eqVlt andbA -ltnNge.
+  rewrite andbC -!andbA -2!negb_or -vFpId orbC -leq_eqVlt -ltnNge.
   have [->|ni0] := eqVneq i; last by rewrite vFpK // eqxx vFp0.
   by case: eqP => // ->; rewrite !andbF.
 rewrite -{2}[mFp]/mFpM -[mFpM _ _]big_split -/mFpM.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 9dddcef..17e3ac4 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -330,9 +330,7 @@ by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF.
 Qed.
 
 Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].
-Proof.
-by elim: m => // m IHm; rewrite !expnS -modnMmr IHm modnMml modnMmr.
-Qed.
+Proof. by elim: m => // m IHm; rewrite !expnS -modnMmr IHm modnMml modnMmr. Qed.
 
 (** Divisibility **)
 
@@ -390,9 +388,7 @@ Lemma dvdn2 n : (2 %| n) = ~~ odd n.
 Proof. by rewrite /dvdn modn2; case (odd n). Qed.
 
 Lemma dvdn_odd m n : m %| n -> odd n -> odd m.
-Proof.
-by move=> m_dv_n; apply: contraTT; rewrite -!dvdn2 => /dvdn_trans->.
-Qed.
+Proof. by move=> m_dv_n; apply: contraTT; rewrite -!dvdn2 => /dvdn_trans->. Qed.
 
 Lemma divnK d m : d %| m -> m %/ d * d = m.
 Proof. by rewrite dvdn_eq; move/eqP. Qed.
@@ -715,9 +711,9 @@ have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT.
 have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0.
 move/IHq=> {IHq} IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d.
   by rewrite mulnDl leq_add // -mulnA leq_mul2l le_kr_n orbT.
-apply: (@addIn d); rewrite -!addnA addnn addnCA mulnDr -addnA addnCA.
-rewrite /km mulnDl mulnCA mulnA -addnA; congr (_ + _).
-by rewrite -def_d addnC -addnA -mulnDl -mulnDr addn_negb -mul2n.
+apply: (@addIn d); rewrite mulnDr -addnA addnACA -def_d addnACA mulnA.
+rewrite -!mulnDl -mulnDr -addnA [kr * _]mulnC; congr addn.
+by rewrite addnC addn_negb muln1 mul2n addnn.
 Qed.
 
 Lemma Bezoutl m n : m > 0 -> {a | a < m & m %| gcdn m n + a * n}.
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index b37ff2c..9fb79a2 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -747,9 +747,7 @@ by move=> x y xp yp; rewrite (orbitE fcycle_undup)// ?mem_rot ?mem_undup.
 Qed.
 
 Lemma eq_order_cycle : {in p &, forall x y, order y = order x}.
-Proof.
-by move=> x y xp yp; rewrite !(order_cycle fcycle_undup) ?mem_undup.
-Qed.
+Proof. by move=> x y xp yp; rewrite !(order_cycle fcycle_undup) ?mem_undup. Qed.
 
 Lemma iter_order_cycle : {in p &, forall x y, iter (order x) f y = y}.
 Proof.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 9953c0d..e608d2b 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -900,7 +900,7 @@ Lemma subDset A B C : (A :\: B \subset C) = (A \subset B :|: C).
 Proof.
 apply/subsetP/subsetP=> sABC x; rewrite !inE.
   by case Bx: (x \in B) => // Ax; rewrite sABC ?inE ?Bx.
-by case Bx: (x \in B) => //; move/sABC; rewrite inE Bx.
+by case Bx: (x \in B) => // /sABC; rewrite inE Bx.
 Qed.
 
 Lemma subsetDP A B C :
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 9ddabcb..67f88a6 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -737,9 +737,7 @@ Proof. by []. Qed.
 
 Lemma properP A B :
   reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B).
-Proof.
-by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn].
-Qed.
+Proof. by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn]. Qed.
 
 Lemma proper_sub A B : A \proper B -> A \subset B.
 Proof. by case/andP. Qed.
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 4eeada9..5ec4037 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -482,7 +482,7 @@ Lemma equiv_sym : symmetric e. Proof. by case: e => [] ? []. Qed.
 Lemma equiv_trans : transitive e. Proof. by case: e => [] ? []. Qed.
 
 Lemma eq_op_trans (T' : eqType) : transitive (@eq_op T').
-Proof. by move=> x y z; move/eqP->; move/eqP->. Qed.
+Proof. by move=> x y z /eqP -> /eqP ->. Qed.
 
 Lemma equiv_ltrans: left_transitive e.
 Proof. by apply: left_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.
@@ -598,8 +598,7 @@ Definition pi := locked (fun x => EquivQuotient (canon_id x)).
 
 Lemma ereprK : cancel erepr pi.
 Proof.
-unlock pi; case=> x hx; move/eqP:(hx)=> hx'.
-exact: (@val_inj _ _ [subType for erepr]).
+by unlock pi; case=> x hx; apply/(@val_inj _ _ [subType for erepr])/eqP.
 Qed.
 
 Local Notation encDE := (encModRelE encD).
@@ -629,9 +628,7 @@ exact/pi_CD.
 Qed.
 
 Lemma equivQTP : cancel (CD \o erepr) (pi \o DC).
-Proof.
-by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP.
-Qed.
+Proof. by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP. Qed.
 
 Local Notation qT := (type_of (Phantom (rel D) encD)).
 Definition quotClass := QuotClass equivQTP.
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 060a2ca..6e72af0 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -1167,7 +1167,7 @@ Qed.
 Lemma cycle_from_next : (forall x, x \in p -> e x (next p x)) -> cycle e p.
 Proof.
 case: p (next p) cycle_next => //= [x q] n; rewrite -(belast_rcons x q x).
-move: {q}(rcons q x) => q n_q; move/allP.
+move: {q}(rcons q x) => q n_q /allP.
 by elim: q x n_q => //= _ q IHq x /andP[/eqP <- n_q] /andP[-> /IHq->].
 Qed.
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 3fe764e..2f35e35 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -289,8 +289,8 @@ apply: apd_ok => //; case: a' def_a le_a_n => [|a'] def_a => [_ | lta] /=.
   rewrite mem_index_iota -(ltn_pmul2r (ltnW lt1q)) -def_r mul1n ltqm /=.
   rewrite -(@ltn_pmul2l p.+2) //; apply: (@leq_ltn_trans m).
     by rewrite def_r mulnC leq_mul.
-  rewrite -addn2 mulnn sqrnD mul2n muln2 -addnn addnCA -addnA addnCA addnA.
-  by rewrite def_a mul1n in def_m; rewrite -def_m addnS -addnA ltnS leq_addr.
+  rewrite -addn2 mulnn sqrnD mul2n muln2 -addnn addnACA.
+  by rewrite def_a mul1n in def_m; rewrite -def_m addnS /= ltnS -addnA leq_addr.
 set bc := ifnz _ _ _; apply: leq_pd_ok (leqnSn _) _.
 rewrite -doubleS -{1}[m]mul1n -[1]/(k.+1.*2.+1 ^ 0)%N.
 apply: IHn; first exact: ltnW.
@@ -436,7 +436,7 @@ Lemma mem_primes p n : (p \in primes n) = [&& prime p, n > 0 & p %| n].
 Proof.
 rewrite andbCA; have [-> // | /= n_gt0] := posnP.
 apply/mapP/andP=> [[[q e]]|[pr_p]] /=.
-  case/mem_prime_decomp=> pr_q e_gt0; case/dvdnP=> u -> -> {p}.
+  case/mem_prime_decomp=> pr_q e_gt0 /dvdnP [u ->] -> {p}.
   by rewrite -(prednK e_gt0) expnS mulnCA dvdn_mulr.
 rewrite [n in _ %| n]prod_prime_decomp // big_seq.
 apply big_ind => [| u v IHu IHv | [q e] /= mem_qe dv_p_qe].
@@ -473,9 +473,7 @@ Lemma pdiv_prime n : 1 < n -> prime (pdiv n).
 Proof. by rewrite -pi_pdiv mem_primes; case/and3P. Qed.
 
 Lemma pdiv_dvd n : pdiv n %| n.
-Proof.
-by case: n (pi_pdiv n) => [|[|n]] //; rewrite mem_primes=> /and3P[].
-Qed.
+Proof. by case: n (pi_pdiv n) => [|[|n]] //; rewrite mem_primes=> /and3P[]. Qed.
 
 Lemma pi_max_pdiv n : (max_pdiv n \in \pi(n)) = (n > 1).
 Proof.
@@ -865,7 +863,7 @@ Proof. by move=> eq_pi n; rewrite 3!inE /= eq_pi. Qed.
 Lemma eq_piP m n : \pi(m) =i \pi(n) <-> \pi(m) = \pi(n).
 Proof.
 rewrite /pi_of; have eqs := eq_sorted_irr ltn_trans ltnn.
-by split=> [|-> //]; move/(eqs _ _ (sorted_primes m) (sorted_primes n)) ->.
+by split=> [|-> //] /(eqs _ _ (sorted_primes m) (sorted_primes n)) ->.
 Qed.
 
 Lemma part_gt0 pi n : 0 < n`_pi.
@@ -938,7 +936,7 @@ Qed.
 Lemma p_part p n : n`_p = p ^ logn p n.
 Proof.
 case (posnP (logn p n)) => [log0 |].
-  by rewrite log0 [n`_p]big1_seq // => q; case/andP; move/eqnP->; rewrite log0.
+  by rewrite log0 [n`_p]big1_seq // => q /andP [/eqP ->]; rewrite log0.
 rewrite logn_gt0 mem_primes; case/and3P=> _ n_gt0 dv_p_n.
 have le_p_n: p < n.+1 by rewrite ltnS dvdn_leq.
 by rewrite [n`_p]big_mkord (big_pred1 (Ordinal le_p_n)).
@@ -1177,7 +1175,7 @@ Proof. by move=> pi'm pi_n; rewrite (pnat_coprime pi'm) ?pnatNK. Qed.
 Lemma sub_pnat_coprime pi rho m n :
   {subset rho <= pi^'} -> pi.-nat m -> rho.-nat n -> coprime m n.
 Proof.
-by move=> pi'rho pi_m; move/(sub_in_pnat (in1W pi'rho)); apply: pnat_coprime.
+by move=> pi'rho pi_m /(sub_in_pnat (in1W pi'rho)); apply: pnat_coprime.
 Qed.
 
 Lemma coprime_partC pi m n : coprime m`_pi n`_pi^'.
@@ -1190,9 +1188,8 @@ Qed.
 
 Lemma part_pnat_id pi n : pi.-nat n -> n`_pi = n.
 Proof.
-case/andP=> n_gt0 pi_n.
-rewrite -[RHS](partnT n_gt0) /partn big_mkcond; apply: eq_bigr=> p _.
-have [->|] := posnP (logn p n); first by rewrite if_same.
+case/andP=> n_gt0 pi_n; rewrite -[RHS]partnT // /partn big_mkcond /=.
+apply: eq_bigr=> p _; have [->|] := posnP (logn p n); first by rewrite if_same.
 by rewrite logn_gt0 => /(allP pi_n)/= ->.
 Qed.
 
@@ -1228,8 +1225,7 @@ Proof. by move=> p_n; exists (logn p n); rewrite -p_part part_pnat_id. Qed.
 
 Lemma pi'_p'nat pi p n : pi^'.-nat n -> p \in pi -> p^'.-nat n.
 Proof.
-move=> pi'n pi_p; apply: sub_in_pnat pi'n => q _.
-by apply: contraNneq => ->.
+by move=> pi'n pi_p; apply: sub_in_pnat pi'n => q _; apply: contraNneq => ->.
 Qed.
  
 Lemma pi_p'nat p pi n : pi.-nat n -> p \in pi^' -> p^'.-nat n.
@@ -1345,7 +1341,7 @@ Lemma modn_partP n a b : 0 < n ->
 Proof.
 move=> n_gt0; wlog le_b_a: a b / b <= a.
   move=> IH; case: (leqP b a) => [|/ltnW] /IH {IH}// IH.
-  by rewrite eq_sym; apply: (iffP IH) => eqab p; move/eqab.
+  by rewrite eq_sym; apply: (iffP IH) => eqab p /eqab.
 rewrite eqn_mod_dvd //; apply: (iffP (dvdn_partP _ n_gt0)) => eqab p /eqab;
   by rewrite -eqn_mod_dvd // => /eqP.
 Qed.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 28b80be..920f393 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -615,14 +615,12 @@ Proof. by rewrite -size_filter filter_predT. Qed.
 Lemma count_predUI a1 a2 s :
   count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
 Proof.
-elim: s => //= x s IHs; rewrite /= addnCA -addnA IHs addnA addnC.
-by rewrite -!addnA; do 2 nat_congr; case (a1 x); case (a2 x).
+elim: s => //= x s IHs; rewrite /= addnACA [RHS]addnACA IHs.
+by case: (a1 x) => //; rewrite addn0.
 Qed.
 
 Lemma count_predC a s : count a s + count (predC a) s = size s.
-Proof.
-by elim: s => //= x s IHs; rewrite addnCA -addnA IHs addnA addn_negb.
-Qed.
+Proof. by elim: s => //= x s IHs; rewrite addnACA IHs; case: (a _). Qed.
 
 Lemma count_filter a1 a2 s : count a1 (filter a2 s) = count (predI a1 a2) s.
 Proof. by rewrite -!size_filter filter_predI. Qed.
@@ -1373,7 +1371,7 @@ Lemma mem_rot s : rot n0 s =i s.
 Proof. by move=> x; rewrite -[s in RHS](cat_take_drop n0) !mem_cat /= orbC. Qed.
 
 Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
-Proof. by apply: inj_eq; apply: rot_inj. Qed.
+Proof. exact/inj_eq/rot_inj. Qed.
 
 End EqSeq.
 
@@ -1967,7 +1965,7 @@ Qed.
 Lemma cat_subseq s1 s2 s3 s4 :
   subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4).
 Proof.
-case/subseqP=> m1 sz_m1 ->; case/subseqP=> m2 sz_m2 ->; apply/subseqP.
+case/subseqP=> m1 sz_m1 -> /subseqP [m2 sz_m2 ->]; apply/subseqP.
 by exists (m1 ++ m2); rewrite ?size_cat ?mask_cat ?sz_m1 ?sz_m2.
 Qed.
 
@@ -2132,9 +2130,7 @@ Lemma map_mask m s : map (mask m s) = mask m (map s).
 Proof. by elim: m s => [|[|] m IHm] [|x p] //=; rewrite IHm. Qed.
 
 Lemma inj_map : injective f -> injective map.
-Proof.
-by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->].
-Qed.
+Proof. by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->]. Qed.
 
 End Map.
 
@@ -2419,9 +2415,7 @@ Lemma size_iota m n : size (iota m n) = n.
 Proof. by elim: n m => //= n IHn m; rewrite IHn. Qed.
 
 Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
-Proof.
-by elim: n1 m => //= [|n1 IHn1] m; rewrite ?addn0 // -addSnnS -IHn1.
-Qed.
+Proof. by elim: n1 m => [|n1 IHn1] m; rewrite ?addn0 // -addSnnS /= -IHn1. Qed.
 
 Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
 Proof. by elim: n m2 => //= n IHn m2; rewrite -addnS IHn. Qed.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index cc22328..39c8451 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -560,9 +560,7 @@ Lemma predn_sub m n : (m - n).-1 = (m.-1 - n).
 Proof. by case: m => // m; rewrite subSKn. Qed.
 
 Lemma leq_sub2r p m n : m <= n -> m - p <= n - p.
-Proof.
-by move=> le_mn; rewrite leq_subLR (leq_trans le_mn) // -leq_subLR.
-Qed.
+Proof. by move=> le_mn; rewrite leq_subLR (leq_trans le_mn) // -leq_subLR. Qed.
 
 Lemma leq_sub2l p m n : m <= n -> p - n <= p - m.
 Proof.
@@ -1283,7 +1281,7 @@ Lemma muln2 m : m * 2 = m.*2.
 Proof. by rewrite mulnC mul2n. Qed.
 
 Lemma doubleD m n : (m + n).*2 = m.*2 + n.*2.
-Proof. by rewrite -!addnn -!addnA (addnCA n). Qed.
+Proof. by rewrite -!mul2n mulnDr. Qed.
 
 Lemma doubleB m n : (m - n).*2 = m.*2 - n.*2.
 Proof. by elim: m n => [|m IHm] []. Qed.
@@ -1704,7 +1702,7 @@ Notation natTrecE := NatTrec.trecE.
 Lemma eq_binP : Equality.axiom N.eqb.
 Proof.
 move=> p q; apply: (iffP idP) => [|<-]; last by case: p => //; elim.
-by case: q; case: p => //; elim=> [p IHp|p IHp|] [q|q|] //=; case/IHp=> ->.
+by case: q; case: p => //; elim=> [p IHp|p IHp|] [q|q|] //= /IHp [->].
 Qed.
 
 Canonical bin_nat_eqMixin := EqMixin eq_binP.
@@ -1813,9 +1811,7 @@ Proof. exact: mk_srt add0n addnC addnA mul1n mul0n mulnC mulnA mulnDl. Qed.
 
 Lemma nat_semi_morph :
   semi_morph 0 1 addn muln (@eq _) 0%num 1%num Nplus Nmult pred1 nat_of_bin.
-Proof.
-by move: nat_of_add_bin nat_of_mul_bin; split=> //= m n; move/eqP->.
-Qed.
+Proof. by move: nat_of_add_bin nat_of_mul_bin; split=> //= m n /eqP ->. Qed.
 
 Lemma nat_power_theory : power_theory 1 muln (@eq _) nat_of_bin expn.
 Proof. by split; apply: nat_of_exp_bin. Qed.