proposition: Lemma gcd_unique_alt : forall n m p, 0<=p -> (forall q, (q|p) <-> (q|n) /\ (q|m)) -> gcd n m == p.
proof: Proof. intros n m p Hp H. apply gcd_unique; trivial. - apply H. apply divide_refl. - apply H. apply divide_refl. - intros. apply H. now split. Qed.
imports: NZAxioms NZMulOrder