From d9421f7dd1f770e1f3767ed1c8e04b741d6abf4b Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Wed, 24 Jul 2024 20:52:13 +0200 Subject: [PATCH] fix for mathcomp master --- theories/numbers/ssetz.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/numbers/ssetz.v b/theories/numbers/ssetz.v index 43e8bda..610efb6 100644 --- a/theories/numbers/ssetz.v +++ b/theories/numbers/ssetz.v @@ -386,7 +386,7 @@ Lemma BZopp_sg x: intp x -> x <> \0z -> Proof. move => pa pb; rewrite /int_np /int_pp. have pnz: (P x <> \0c) by move => h; case: pb; apply: BZ_0_if_val0. -by rewrite /BZopp /BZ_of_nat /BZm_of_nat; Ytac0;Ytac sx; aw; rewrite ? sx. +by rewrite /BZopp /BZ_of_nat /BZm_of_nat; Ytac0;Ytac sx; aw; rewrite ? sx; split. Qed. Lemma BZopp_positive1 x: inc x BZps -> inc (BZopp x) BZms.