fix

math-comp · Sep 5, 2022 · ce7f6b2 · ce7f6b2
1 parent fd48780
commit ce7f6b2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v
@@ -149,10 +149,10 @@ Lemma eqbRL (b1 b2 : bool) : b1 = b2 -> b2 -> b1.
 Proof. by move->. Qed.
 
 Lemma natrS (R : ringType) (n : nat) : (n.+1%:R = n%:R + 1 :> R)%R.
-Proof. by rewrite -addn1 GRing.natrD. Qed.
+Proof. by rewrite GRing.mulrSr. Qed.
 
 Lemma natSr (R : ringType) (n : nat) : (n.+1%:R = 1 + n%:R :> R)%R.
-Proof. by rewrite -add1n GRing.natrD. Qed.
+Proof. by rewrite GRing.mulrS. Qed.
 
 (***************************)
 (* MathComp 1.15 additions *)