proposition: Lemma lcm_divide_iff : forall n m p, (lcm n m | p) <-> (n | p) /\ (m | p).
proof: Proof. intros n m p. split;[split|]. - transitivity (lcm n m); trivial using divide_lcm_l. - transitivity (lcm n m); trivial using divide_lcm_r. - intros (H,H'). now apply lcm_least. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor