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