proposition: Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0.
proof: Proof. intros n m. split. - split. + now apply gcd_eq_0_l with m. + now apply gcd_eq_0_r with n. - intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg. Qed.
imports: NZAxioms NZMulOrder