Z.div_mod_to_equations, Z.quot_rem_to_equations, Z.to_euclidean_division_equations: the tactics for preprocessing Z.div and Z.modulo, Z.quot and Z.rem
These tactic use the complete specification of
Z.div and
Z.modulo (
Z.quot and
Z.rem, respectively) to remove these
functions from the goal without losing information. The
Z.euclidean_division_equations_cleanup tactic removes needless
hypotheses, which makes tactics like
nia run faster. The tactic
Z.to_euclidean_division_equations combines the handling of both variants
of division/quotient and modulo/remainder.