4 files changed, 22 insertions, 17 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index c260105..06774ff 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -45,7 +45,7 @@ transitivity (\sum_(1 <= i < n.+1) \sum_(1 <= k < n.+1) (p ^ k %| i)).
   by apply: andb_idr => /dvdn_leq/(leq_trans (ltn_expl _ (prime_gt1 _)))->.
 by rewrite exchange_big_nat; apply: eq_bigr => i _; rewrite divn_count_dvd.
 Qed.
- 
+
 Theorem Wilson p : p > 1 -> prime p = (p %| ((p.-1)`!).+1).
 Proof.
 have dFact n: 0 < n -> (n.-1)`! = \prod_(0 <= i < n | i != 0) i.
@@ -310,7 +310,7 @@ Qed.
 Lemma subn_exp m n k :
   m ^ k - n ^ k = (m - n) * (\sum_(i < k) m ^ (k.-1 -i) * n ^ i).
 Proof.
-case: k => [|k]; first by rewrite big_ord0.
+case: k => [|k]; first by rewrite big_ord0 muln0.
 rewrite mulnBl !big_distrr big_ord_recl big_ord_recr /= subn0 muln1.
 rewrite subnn mul1n -!expnS subnDA; congr (_ - _); apply: canRL (addnK _) _.
 congr (_ + _); apply: eq_bigr => i _.
@@ -543,4 +543,3 @@ by apply: val_inj; congr (_ :: _); apply: val_inj; rewrite /= -{1}def_n addnK.
 Qed.
 
 End Combinations.
-
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index fda425d..3cb98e8 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -538,7 +538,7 @@ Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n.
 Proof. by rewrite addnC gcdnDl. Qed.
 
 Lemma gcdnMl n m : gcdn n (m * n) = n.
-Proof. by case: n => [|n]; rewrite gcdnE modnMl gcd0n. Qed.
+Proof. by case: n => [|n]; rewrite gcdnE modnMl // muln0. Qed.
 
 Lemma gcdnMr n m : gcdn n (n * m) = n.
 Proof. by rewrite mulnC gcdnMl. Qed.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 3685c23..76acaca 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -497,7 +497,7 @@ Lemma all_nseqb (b : bool) x : all (nseq b x) = b ==> a x.
 Proof. by rewrite all_nseq eqb0 implybE. Qed.
 
 Lemma find_nseq n x : find (nseq n x) = ~~ a x * n.
-Proof. by elim: n => //= n ->; case: (a x). Qed.
+Proof. by elim: n => /= [|n ->]; case: (a x). Qed.
 
 Lemma nth_find s : has s -> a (nth s (find s)).
 Proof. by elim: s => //= x s IHs; case Hx: (a x). Qed.
@@ -928,7 +928,7 @@ Proof. by rewrite -size_eq0 size_filter has_count lt0n. Qed.
 Fixpoint mem_seq (s : seq T) :=
   if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.
 
-Definition seq_eqclass := seq T. 
+Definition seq_eqclass := seq T.
 Identity Coercion seq_of_eqclass : seq_eqclass >-> seq.
 Coercion pred_of_seq (s : seq_eqclass) : {pred T} := mem_seq s.
 
@@ -3068,4 +3068,3 @@ Notation perm_uniq :=
       deprecate perm_uniq eq_uniq T s1 s2 eq_sz12 eq_s12)
     _ _ _)
   (only parsing).
-
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 86f8fb2..ad44d3b 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -106,6 +106,10 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+(* Disable Coq prelude hints to improve proof script robustness. *)
+
+Remove Hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm : core.
+
 (* Declare legacy Arith operators in new scope. *)
 
 Delimit Scope coq_nat_scope with coq_nat.
@@ -200,7 +204,7 @@ Lemma add1n n : 1 + n = n.+1.            Proof. by []. Qed.
 
 Lemma addn0 : right_id 0 addn. Proof. by move=> n; apply/eqP; elim: n. Qed.
 
-Lemma addnS m n : m + n.+1 = (m + n).+1. Proof. by elim: m. Qed.
+Lemma addnS m n : m + n.+1 = (m + n).+1. Proof. by apply/eqP; elim: m. Qed.
 
 Lemma addSnnS m n : m.+1 + n = m + n.+1. Proof. by rewrite addnS. Qed.
 
@@ -831,7 +835,7 @@ Proof. by move=> eq_op x; apply: eq_iteri; case. Qed.
 End Iteration.
 
 Lemma iter_succn m n : iter n succn m = m + n.
-Proof. by elim: n => //= n ->. Qed.
+Proof. by rewrite addnC; elim: n => //= n ->. Qed.
 
 Lemma iter_succn_0 n : iter n succn 0 = n.
 Proof. exact: iter_succn. Qed.
@@ -1637,24 +1641,27 @@ case=> //=; elim=> //= p; case: (nat_of_pos p) => //= n [<-].
 by rewrite natTrecE addnS /= addnS {2}addnn; elim: {1 3}n.
 Qed.
 
-Lemma nat_of_succ_gt0 p : Pos.succ p = p.+1 :> nat.
+Lemma nat_of_succ_pos p : Pos.succ p = p.+1 :> nat.
 Proof. by elim: p => //= p ->; rewrite !natTrecE. Qed.
 
-Lemma nat_of_addn_gt0 p q : (p + q)%positive = p + q :> nat.
+Lemma nat_of_add_pos p q : (p + q)%positive = p + q :> nat.
 Proof.
 apply: @fst _ (Pplus_carry p q = (p + q).+1 :> nat) _.
 elim: p q => [p IHp|p IHp|] [q|q|] //=; rewrite !natTrecE //;
-  by rewrite ?IHp ?nat_of_succ_gt0 ?(doubleS, doubleD, addn1, addnS).
+  by rewrite ?IHp ?nat_of_succ_pos ?(doubleS, doubleD, addn1, addnS).
+Qed.
+
+Lemma nat_of_mul_pos p q : (p * q)%positive = p * q :> nat.
+Proof.
+elim: p => [p IHp|p IHp|] /=; rewrite ?mul1n //;
+  by rewrite ?nat_of_add_pos /= !natTrecE IHp doubleMl.
 Qed.
 
 Lemma nat_of_add_bin b1 b2 : (b1 + b2)%num = b1 + b2 :> nat.
-Proof. by case: b1 b2 => [|p] [|q] //=; apply: nat_of_addn_gt0. Qed.
+Proof. by case: b1 b2 => [|p] [|q]; rewrite ?addn0 //= nat_of_add_pos. Qed.
 
 Lemma nat_of_mul_bin b1 b2 : (b1 * b2)%num = b1 * b2 :> nat.
-Proof.
-case: b1 b2 => [|p] [|q] //=; elim: p => [p IHp|p IHp|] /=;
-  by rewrite ?(mul1n, nat_of_addn_gt0, mulSn) //= !natTrecE IHp doubleMl.
-Qed.
+Proof. by case: b1 b2 => [|p] [|q]; rewrite ?muln0 //= nat_of_mul_pos. Qed.
 
 Lemma nat_of_exp_bin n (b : N) : n ^ b = pow_N 1 muln n b.
 Proof.