Stop relying on replace by automatic assumption-based solving

Before coq/coq#17964 `replace foo with bar by tac` actually means
`replace foo with bar by first [assumption | symmetry; assumption | tac]`.

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.
- replace (NN.to_Z q) with 0%Z in * by assumption.
+ rewrite e in *.
  rewrite Zdiv_0_l in *; auto with zarith.
  apply Zgcd_div_swap0; lia.
  (* Gt *)