fix for mathcomp master

coq-community · Jul 24, 2024 · d9421f7 · d9421f7
1 parent bca0798
commit d9421f7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.