proposition: Lemma lcm_unique_alt : forall n m p, 0<=p -> (forall q, (p|q) <-> (n|q) /\ (m|q)) -> lcm n m == p.
proof: Proof. intros n m p Hp H. apply lcm_unique; trivial. - apply H, divide_refl. - apply H, divide_refl. - intros. apply H. now split. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor