proposition: Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n).
proof: Proof. intros n m Hn. split. - intros (q,Hq). rewrite Hq. rewrite mul_comm. now apply gcd_mul_diag_l. - intros EQ. rewrite <- EQ. apply gcd_divide_r. Qed.
imports: NZAxioms NZMulOrder