From fc340bc0503e1908ad15d68f381cd1869088e39f Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 5 Aug 2024 14:27:17 +0200 Subject: [PATCH] adapt to MC#1256 --- theories/zify_algebra.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v index 47215ff..6fe1ec1 100644 --- 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) :=