proposition: Lemma divide_lcm_eq_r : forall n m, 0<=m -> (n|m) -> lcm n m == m.
proof: Proof. intros n m Hm H. apply lcm_unique_alt; trivial. intros q. split. - split; trivial. now transitivity m. - now destruct 1. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor