Merge pull request #56 from Tragicus/pr1256

adapt to MC#1256
math-comp · Aug 14, 2024 · b25e4e5 · b25e4e5
2 parents 3ea1c2d + fc340bc
commit b25e4e5
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) :=