adapt to MC#1256

math-comp · Aug 9, 2024 · fc340bc · fc340bc
1 parent 3ea1c2d
commit fc340bc
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v
@@ -341,7 +341,10 @@ 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); first by lia.
+by move=> ->; lia.
+Qed.
 
 #[global]
 Instance Op_Z_natmul : BinOp (@GRing.natmul _ : Z -> nat -> Z) :=