proposition: Lemma lcm_eq_0 : forall n m, lcm n m == 0 <-> n == 0 \/ m == 0.
proof: Proof. intros. split. - intros EQ. apply eq_mul_0. apply divide_0_l. rewrite <- EQ. apply lcm_least. + apply divide_factor_l. + apply divide_factor_r. - destruct 1 as [EQ|EQ]; rewrite EQ. + apply lcm_0_l. + apply lcm_0_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor