Merge pull request #80 from SkySkimmer/replace

Better fix for coq/coq#17964: use correct direction of assumption
coq-community · Sep 8, 2023 · 9b7f830 · 9b7f830
2 parents b06cf12 + e78b257
commit 9b7f830
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/BigQ/QMake.v b/BigQ/QMake.v
@@ -226,7 +226,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  rewrite strong_spec_check_int.
  qsimpl.
  generalize (Zgcd_div_pos (ZZ.to_Z p) (NN.to_Z q)). lia.
- rewrite e in *.
+ replace (NN.to_Z q) with 0%Z in * by (symmetry; assumption).
  rewrite Zdiv_0_l in *; auto with zarith.
  apply Zgcd_div_swap0; lia.
  (* Gt *)