proposition: Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 -> a * (b / gcd a b) == (a*b)/gcd a b.
proof: Proof. intros a b H. rewrite divide_div_mul_exact; try easy. apply gcd_divide_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor