proposition: Lemma divide_lcm_r : forall a b, (b | lcm a b).
proof: Proof. unfold lcm. intros a b. apply divide_abs_r. rewrite <- gcd_div_swap. apply divide_factor_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor