Merge pull request #504 from pi8027/selectors

Revise proofs in ssreflect/*.v

mathcomp/ssreflect/bigop.v

@@ -854,7 +854,7 @@ Proof. by rewrite unlock; elim: r => //= j r ->. Qed.
 Lemma big_nth x0 r (P : pred I) F :
   \big[op/idx]_(i <- r | P i) F i
      = \big[op/idx]_(0 <= i < size r | P (nth x0 r i)) (F (nth x0 r i)).
-Proof. by rewrite -{1}(mkseq_nth x0 r) big_map /index_iota subn0. Qed.
+Proof. by rewrite -[r in LHS](mkseq_nth x0) big_map /index_iota subn0. Qed.
 
 Lemma big_hasC r (P : pred I) F :
   ~~ has P r -> \big[op/idx]_(i <- r | P i) F i = idx.
@@ -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.
@@ -1548,10 +1546,10 @@ Lemma pair_big_dep (I J : finType) (P : pred I) (Q : I -> pred J) F :
   \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j =
     \big[*%M/1]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.
 Proof.
-rewrite (partition_big (fun p => p.1) P) => [|j]; last by case/andP.
-apply: eq_bigr => i /= Pi; rewrite (reindex_onto (pair i) (fun p => p.2)).
+rewrite (partition_big fst P) => [|j]; last by case/andP.
+apply: eq_bigr => i /= Pi; rewrite (reindex_onto (pair i) snd).
    by apply: eq_bigl => j; rewrite !eqxx [P i]Pi !andbT.
-by case=> i' j /=; case/andP=> _ /=; move/eqP->.
+by case=> i' j /= /andP [_] /eqP ->.
 Qed.
 
 Lemma pair_big (I J : finType) (P : pred I) (Q : pred J) F :

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).
@@ -90,16 +89,16 @@ have le_pmFp (i : 'I_p) m: i <= p + m.
 have eqFp (i j : 'I_p): (i == j) = (p %| p + i - j).
   by rewrite -eqn_mod_dvd ?(modnDl, Fp_mod).
 have vFpId i: (vFp i == i :> nat) = xpred2 Fp1 Fpn1 i.
-  symmetry; have [->{i} | /eqP ni0] := i =P Fp0.
-    by rewrite /= -!val_eqE /= -{2}[p]prednK //= modn_small //= -(subnKC lt1p).
-  rewrite 2!eqFp -Euclid_dvdM //= -[_ - p.-1]subSS prednK //.
+  have [->{i} | ni0] := eqVneq i Fp0.
+    by rewrite -!val_eqE /= egcd0n modn_small //= -(subnKC lt1p).
+  rewrite 2!eqFp -Euclid_dvdM // -[_ - p.-1]subSS prednK //.
   have lt0i: 0 < i by rewrite lt0n.
   rewrite -addnS addKn -addnBA // mulnDl -{2}(addn1 i) -subn_sqr.
   rewrite addnBA ?leq_sqr // mulnS -addnA -mulnn -mulnDl.
   rewrite -(subnK (le_pmFp (vFp i) i)) mulnDl addnCA.
   rewrite -[1 ^ 2]/(Fp1 : nat) -addnBA // dvdn_addl.
     by rewrite Euclid_dvdM // -eqFp eq_sym orbC /dvdn Fp_mod eqn0Ngt lt0i.
-  by rewrite -eqn_mod_dvd // Fp_mod modnDl -(vFpV _ ni0) eqxx.
+  by rewrite -eqn_mod_dvd // Fp_mod modnDl -(vFpV _ ni0).
 suffices [mod_fact]: toFp (p.-1)`! = Fpn1.
   by rewrite /dvdn -addn1 -modnDml mod_fact addn1 prednK // modnn.
 rewrite dFact //; rewrite ((big_morph toFp) Fp1 mFpM) //; first last.
@@ -113,12 +112,11 @@ 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.
-  rewrite andbA -ltnNge; symmetry; have [->|ni0] := eqVneq.
-    by case: eqP => // E; rewrite ?E !andbF.
-  by rewrite vFpK //eqxx vFp0.
+  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.
-by rewrite big1 ?mFp1r //= => i /andP[]; auto.
+by rewrite big1 ?mFp1r //= => i /andP [/vFpV].
 Qed.
 
 (** The falling factorial *)
@@ -326,7 +324,7 @@ Qed.
 
 Lemma predn_exp m k : (m ^ k).-1 = m.-1 * (\sum_(i < k) m ^ i).
 Proof.
-rewrite -!subn1 -{1}(exp1n k) subn_exp; congr (_ * _).
+rewrite -!subn1 -[in LHS](exp1n k) subn_exp; congr (_ * _).
 symmetry; rewrite (reindex_inj rev_ord_inj); apply: eq_bigr => i _ /=.
 by rewrite -subn1 -subnDA exp1n muln1.
 Qed.
@@ -368,8 +366,7 @@ elim: n A => [|n IHn] A.
   by rewrite (@eq_card1 _ [tuple]) // => t; rewrite [t]tuple0 inE.
 rewrite -sum1dep_card (partition_big (@thead _ _) A) /= => [|t]; last first.
   by case/tupleP: t => x t; do 2!case/andP.
-transitivity (#|A| * #|A|.-1 ^_ n)%N; last by case: #|A|.
-rewrite -sum_nat_const; apply: eq_bigr => x Ax.
+rewrite ffactnS -sum_nat_const; apply: eq_bigr => x Ax.
 rewrite (cardD1 x) [x \in A]Ax /= -(IHn [predD1 A & x]) -sum1dep_card.
 rewrite (reindex (fun t : n.-tuple T => [tuple of x :: t])) /=; last first.
   pose ttail (t : n.+1.-tuple T) := [tuple of behead t].
@@ -428,7 +425,7 @@ rewrite (reindex (fun p : {ffun _} => [ffun i => f0 (p i)])) /=; last first.
   rewrite -im_f0 => /andP[/andP[/ffun_onP f_ffun /injectiveP injf] /eqP im_f].
   apply/ffunP=> i; rewrite !ffunE /ff0'; case: pickP => [y /eqP //|].
   have /imsetP[j _ eq_f0j_fi]: f i \in f0 @: 'I_k by rewrite -im_f mem_imset.
-  by move/(_ j)=> /eqP[].
+  by move/(_ j)/eqP.
 rewrite -ffactnn -card_inj_ffuns -sum1dep_card; apply: eq_bigl => p.
 rewrite -andbA.
 apply/and3P/injectiveP=> [[_ /injectiveP inj_f0p _] i j eq_pij | inj_p].
@@ -454,7 +451,7 @@ Proof.
 have [-> | n_gt0] := posnP n; last pose i0 := Ordinal n_gt0.
   case: m => [|m]; last by apply: eq_card0; case/tupleP=> [[]].
   by apply: (@eq_card1 _ [tuple]) => t; rewrite [t]tuple0 inE.
-rewrite -{12}[n]card_ord -card_draws.
+rewrite -[n in RHS]card_ord -card_draws.
 pose f_t (t : m.-tuple 'I_n) := [set i in t].
 pose f_A (A : {set 'I_n}) := [tuple of mkseq (nth i0 (enum A)) m].
 have val_fA (A : {set 'I_n}) : #|A| = m -> val (f_A A) = enum A.
@@ -465,13 +462,13 @@ have inc_A (A : {set 'I_n}) : sorted ltn (map val (enum A)).
   by rewrite (sorted_filter ltn_trans) // unlock val_ord_enum iota_ltn_sorted.
 rewrite -!sum1dep_card (reindex_onto f_t f_A) /= => [|A]; last first.
   by move/eqP=> cardAm; apply/setP=> x; rewrite inE -(mem_enum (mem A)) -val_fA.
-apply: eq_bigl => t; apply/idP/idP=> [inc_t|]; last first.
-  by case/andP; move/eqP=> t_m; move/eqP=> <-; rewrite val_fA.
+apply: eq_bigl => t.
+apply/idP/idP => [inc_t|/andP [/eqP t_m /eqP <-]]; last by rewrite val_fA.
 have ft_m: #|f_t t| = m.
   rewrite cardsE (card_uniqP _) ?size_tuple // -(map_inj_uniq val_inj).
   exact: (sorted_uniq ltn_trans ltnn).
 rewrite ft_m eqxx -val_eqE val_fA // -(inj_eq (inj_map val_inj)) /=.
-apply/eqP; apply: (eq_sorted_irr ltn_trans ltnn) => // y.
+apply/eqP/(eq_sorted_irr ltn_trans ltnn) => // y.
 by apply/mapP/mapP=> [] [x t_x ->]; exists x; rewrite // mem_enum inE in t_x *.
 Qed.
 
@@ -488,11 +485,11 @@ have add_mnC t: val \o add_mn t =1 add_mn_nat t \o val.
 pose f_add t := [tuple of map (add_mn t) (ord_tuple m)].
 rewrite -card_ltn_sorted_tuples -!sum1dep_card (reindex f_add) /=.
   apply: eq_bigl => t; rewrite -map_comp (eq_map (add_mnC t)) map_comp.
-  rewrite enumT unlock val_ord_enum -{1}(drop0 t).
+  rewrite enumT unlock val_ord_enum -[in LHS](drop0 t).
   have [m0 | m_gt0] := posnP m.
     by rewrite {2}m0 /= drop_oversize // size_tuple m0.
   have def_m := subnK m_gt0; rewrite -{2}def_m addn1 /= {1}/add_mn_nat.
-  move: 0 (m - 1) def_m => i k; rewrite -{1}(size_tuple t) => def_m.
+  move: 0 (m - 1) def_m => i k; rewrite -[in RHS](size_tuple t) => def_m.
   rewrite (drop_nth x0) /=; last by rewrite -def_m leq_addl.
   elim: k i (nth x0 t i) def_m => [|k IHk] i x /=.
     by rewrite add0n => ->; rewrite drop_size.

mathcomp/ssreflect/choice.v

@@ -82,7 +82,7 @@ Definition decode n := if n is 0 then [::] else [rec 0, n.-1, n.-1].
 Lemma decodeK : cancel decode code.
 Proof.
 have m2s: forall n, n.*2 - n = n by move=> n; rewrite -addnn addnK.
-case=> //= n; rewrite -[n.+1]mul1n -(expn0 2) -{3}[n]m2s.
+case=> //= n; rewrite -[n.+1]mul1n -(expn0 2) -[n in RHS]m2s.
 elim: n {2 4}n {1 3}0 => [|q IHq] [|[|r]] v //=; rewrite {}IHq ?mul1n ?m2s //.
 by rewrite expnSr -mulnA mul2n.
 Qed.
@@ -336,10 +336,9 @@ Lemma eq_xchoose P Q exP exQ : P =1 Q -> @xchoose P exP = @xchoose Q exQ.
 Proof.
 rewrite /xchoose => eqPQ.
 case: (xchoose_subproof exP) => x; case: (xchoose_subproof exQ) => y /=.
-case: ex_minnP => n; case: ex_minnP => m.
-rewrite -(extensional eqPQ) {1}(extensional eqPQ).
-move=> Qm minPm Pn minQn; suffices /eqP->: m == n by move=> -> [].
-by rewrite eqn_leq minQn ?minPm.
+case: ex_minnP => n; rewrite -(extensional eqPQ) => Pn minQn.
+case: ex_minnP => m; rewrite !(extensional eqPQ) => Qm minPm.
+by case: (eqVneq m n) => [-> -> [] //|]; rewrite eqn_leq minQn ?minPm.
 Qed.
 
 Lemma sigW P : (exists x, P x) -> {x | P x}.

mathcomp/ssreflect/div.v

@@ -51,8 +51,8 @@ Proof.
 move=> lt_rd; have d_gt0: 0 < d by apply: leq_trans lt_rd.
 case: edivnP lt_rd => q' r'; rewrite d_gt0 /=.
 wlog: q q' r r' / q <= q' by case/orP: (leq_total q q'); last symmetry; eauto.
-rewrite leq_eqVlt; case/predU1P => [-> /addnI-> |] //=.
-rewrite -(leq_pmul2r d_gt0) => /leq_add lt_qr eq_qr _ /lt_qr {lt_qr}.
+have [||-> _ /addnI ->] //= := ltngtP q q'.
+rewrite -(leq_pmul2r d_gt0) => /leq_add lt_qr _ eq_qr _ /lt_qr {lt_qr}.
 by rewrite addnS ltnNge mulSn -addnA eq_qr addnCA addnA leq_addr.
 Qed.
 
@@ -189,7 +189,7 @@ rewrite {}/offset; case: d => // d _; rewrite /divn !modn_def.
 case: (edivnP m d.+1) (edivnP n d.+1) => [/= q r -> r_lt] [/= p s -> s_lt].
 rewrite addnACA -mulnDl; have [r_le s_le] := (ltnW r_lt, ltnW s_lt).
 have [d_ge|d_lt] := leqP; first by rewrite addn0 mul0n subn0 edivn_eq.
-rewrite addn1 mul1n -{1}(subnKC d_lt) addnA -mulSnr edivn_eq//.
+rewrite addn1 mul1n -[in LHS](subnKC d_lt) addnA -mulSnr edivn_eq//.
 by rewrite ltn_subLR// -addnS leq_add.
 Qed.
 
@@ -256,8 +256,8 @@ Proof. by case: d => // d; apply: modn_small; rewrite ltn_mod. Qed.
 
 Lemma modnMDl p m d : p * d + m = m %[mod d].
 Proof.
-case: (posnP d) => [-> | d_gt0]; first by rewrite muln0.
-by rewrite {1}(divn_eq m d) addnA -mulnDl modn_def edivn_eq // ltn_mod.
+have [->|d_gt0] := posnP d; first by rewrite muln0.
+by rewrite [in LHS](divn_eq m d) addnA -mulnDl modn_def edivn_eq // ltn_mod.
 Qed.
 
 Lemma muln_modr p m d : p * (m %% d) = (p * m) %% (p * d).
@@ -278,27 +278,24 @@ by rewrite mulSnr -addnS leq_add ?leq_mul2r.
 Qed.
 
 Lemma modnDl m d : d + m = m %[mod d].
-Proof. by rewrite -{1}[d]mul1n modnMDl. Qed.
+Proof. by rewrite -[m %% _](modnMDl 1) mul1n. Qed.
 
-Lemma modnDr m d : m + d = m %[mod d].
-Proof. by rewrite addnC modnDl. Qed.
+Lemma modnDr m d : m + d = m %[mod d]. Proof. by rewrite addnC modnDl. Qed.
 
-Lemma modnn d : d %% d = 0.
-Proof. by rewrite -[d in d %% _]addn0 modnDl mod0n. Qed.
+Lemma modnn d : d %% d = 0. Proof. by rewrite [d %% d](modnDr 0) mod0n. Qed.
 
 Lemma modnMl p d : p * d %% d = 0.
 Proof. by rewrite -[p * d]addn0 modnMDl mod0n. Qed.
 
-Lemma modnMr p d : d * p %% d = 0.
-Proof. by rewrite mulnC modnMl. Qed.
+Lemma modnMr p d : d * p %% d = 0. Proof. by rewrite mulnC modnMl. Qed.
 
 Lemma modnDml m n d : m %% d + n = m + n %[mod d].
 Proof. by rewrite [in RHS](divn_eq m d) -addnA modnMDl. Qed.
 
 Lemma modnDmr m n d : m + n %% d = m + n %[mod d].
 Proof. by rewrite !(addnC m) modnDml. Qed.
 
-Lemma modnDm m n d : m %% d  + n %% d = m + n %[mod d].
+Lemma modnDm m n d : m %% d + n %% d = m + n %[mod d].
 Proof. by rewrite modnDml modnDmr. Qed.
 
 Lemma eqn_modDl p m n d : (p + m == p + n %[mod d]) = (m == n %[mod d]).
@@ -333,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 **)
 
@@ -393,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.
@@ -440,8 +433,8 @@ Proof. by move=> n_gt0 lt_nd; rewrite /dvdn eqn0Ngt modn_small ?n_gt0. Qed.
 
 Lemma eqn_dvd m n : (m == n) = (m %| n) && (n %| m).
 Proof.
-case: m n => [|m] [|n] //; apply/idP/andP; first by move/eqP->; auto.
-rewrite eqn_leq => [[Hmn Hnm]]; apply/andP; have:= dvdn_leq; auto.
+case: m n => [|m] [|n] //; apply/idP/andP => [/eqP -> //| []].
+by rewrite eqn_leq => Hmn Hnm; do 2 rewrite dvdn_leq //.
 Qed.
 
 Lemma dvdn_pmul2l p d m : 0 < p -> (p * d %| p * m) = (d %| m).
@@ -507,8 +500,8 @@ Proof. by case: k => // k _ d_dv_m; rewrite expnS dvdn_mulr. Qed.
 
 Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
 Proof.
-case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
-by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
+case: m => //= m; elim: n => //= n IHn; rewrite ltnS.
+have [/IHn/dvdn_mull->||-> _] // := ltngtP m n; exact: dvdn_mulr.
 Qed.
 
 Hint Resolve dvdn_add dvdn_sub dvdn_exp : core.
@@ -567,7 +560,7 @@ Proof.
 rewrite -subn1; case: d m => [|[|d]] [|m]//= _ _.
   by rewrite ?modn1 ?dvd1n ?modn0 ?subn1.
 rewrite modnB// (@modn_small 1)// [_ < _]leqn0 /dvdn mulnbl/= subn1.
-by case: ifP => // /eqP->; rewrite addn0.
+by case: eqP => // ->; rewrite addn0.
 Qed.
 
 Lemma edivn_pred m d : d != 1 -> 0 < m ->
@@ -601,8 +594,7 @@ Proof. by case=> // n; rewrite gcdnE modnn. Qed.
 
 Lemma gcdnC : commutative gcdn.
 Proof.
-move=> m n; wlog lt_nm: m n / n < m.
-  by case: (ltngtP n m) => [||-> //]; last symmetry; auto.
+move=> m n; wlog lt_nm: m n / n < m by have [? ->|? <-|-> //] := ltngtP n m.
 by rewrite gcdnE -[in m == 0](ltn_predK lt_nm) modn_small.
 Qed.
 
@@ -719,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}.
@@ -741,7 +733,7 @@ Lemma dvdn_gcd p m n : p %| gcdn m n = (p %| m) && (p %| n).
 Proof.
 apply/idP/andP=> [dv_pmn | [dv_pm dv_pn]].
   by rewrite !(dvdn_trans dv_pmn) ?dvdn_gcdl ?dvdn_gcdr.
-case (posnP n) => [->|n_gt0]; first by rewrite gcdn0.
+have [->|n_gt0] := posnP n; first by rewrite gcdn0.
 case: (Bezoutr m n_gt0) => // km _ /(dvdn_trans dv_pn).
 by rewrite dvdn_addl // dvdn_mull.
 Qed.
@@ -765,7 +757,7 @@ Proof. by move=> m n p q; rewrite -!gcdnA (gcdnCA n). Qed.
 
 Lemma muln_gcdr : right_distributive muln gcdn.
 Proof.
-move=> p m n; case: (posnP p) => [-> //| p_gt0].
+move=> p m n; have [-> //|p_gt0] := posnP p.
 elim/ltn_ind: m n => m IHm n; rewrite gcdnE [RHS]gcdnE muln_eq0 (gtn_eqF p_gt0).
 by case: posnP => // m_gt0; rewrite -muln_modr //=; apply/IHm/ltn_pmod.
 Qed.
@@ -988,7 +980,7 @@ Qed.
 Lemma dvdn_pexp2r m n k : k > 0 -> (m ^ k %| n ^ k) = (m %| n).
 Proof.
 move=> k_gt0; apply/idP/idP=> [dv_mn_k|]; last exact: dvdn_exp2r.
-case: (posnP n) => [-> | n_gt0]; first by rewrite dvdn0.
+have [->|n_gt0] := posnP n; first by rewrite dvdn0.
 have [n' def_n] := dvdnP (dvdn_gcdr m n); set d := gcdn m n in def_n.
 have [m' def_m] := dvdnP (dvdn_gcdl m n); rewrite -/d in def_m.
 have d_gt0: d > 0 by rewrite gcdn_gt0 n_gt0 orbT.
@@ -1013,7 +1005,7 @@ Lemma chinese_remainder x y :
   (x == y %[mod m1 * m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).
 Proof.
 wlog le_yx : x y / y <= x; last by rewrite !eqn_mod_dvd // Gauss_dvd.
-by case/orP: (leq_total y x); last rewrite !(eq_sym (x %% _)); auto.
+by have [?|/ltnW ?] := leqP y x; last rewrite !(eq_sym (x %% _)); apply.
 Qed.
 
 (***********************************************************************)

mathcomp/ssreflect/eqtype.v

@@ -409,7 +409,7 @@ Lemma bij_eq : bijective f -> forall x y, (f x == f y) = (x == y).
 Proof. by move/bij_inj; apply: inj_eq. Qed.
 
 Lemma can2_eq : cancel f g -> cancel g f -> forall x y, (f x == y) = (x == g y).
-Proof. by move=> fK gK x y; rewrite -{1}[y]gK; apply: can_eq. Qed.
+Proof. by move=> fK gK x y; rewrite -[y in LHS]gK; apply: can_eq. Qed.
 
 Lemma inj_in_eq :
   {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)}.