proposition: Lemma gcd_unique : forall n m p, 0<=p -> (p|n) -> (p|m) -> (forall q, (q|n) -> (q|m) -> (q|p)) -> gcd n m == p.
proof: Proof. intros n m p Hp Hn Hm H. apply divide_antisym_nonneg; trivial. - apply gcd_nonneg. - apply H. + apply gcd_divide_l. + apply gcd_divide_r. - now apply gcd_greatest. Qed.
imports: NZAxioms NZMulOrder