proposition: Lemma gcd_divide_iff : forall n m p, (p | gcd n m) <-> (p | n) /\ (p | m).
proof: Proof. intros n m p. split. - split. + transitivity (gcd n m); trivial using gcd_divide_l. + transitivity (gcd n m); trivial using gcd_divide_r. - intros (H,H'). now apply gcd_greatest. Qed.
imports: NZAxioms NZMulOrder