adapt to MC#1256

math-comp · Aug 5, 2024 · ff3aedc · ff3aedc
1 parent 3ea1c2d
commit ff3aedc
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v
@@ -341,7 +341,11 @@ Instance Op_Z_mulr : BinOp ( *%R : Z -> Z -> Z) :=
 Add Zify BinOp Op_Z_mulr.
 
 Fact Op_Z_natmul_subproof (n : Z) (m : nat) : (n *+ m)%R = (n * Z.of_nat m)%Z.
-Proof. elim: m => [|m]; rewrite (mulr0n, mulrS); lia. Qed.
+Proof.
+elim: m => [|m]; rewrite (mulr0n, mulrS).
+  by lia.
+by move=> ->; lia.
+Qed.
 
 #[global]
 Instance Op_Z_natmul : BinOp (@GRing.natmul _ : Z -> nat -> Z) :=