proposition: Lemma lcm_unique : forall n m p, 0<=p -> (n|p) -> (m|p) -> (forall q, (n|q) -> (m|q) -> (p|q)) -> lcm n m == p.
proof: Proof. intros n m p Hp Hn Hm H. apply divide_antisym_nonneg; trivial. - apply lcm_nonneg. - now apply lcm_least. - apply H. + apply divide_lcm_l. + apply divide_lcm_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor