proposition: Lemma gcd_mul_diag_l : forall n m, 0<=n -> gcd n (n*m) == n.
proof: Proof. intros n m Hn. apply gcd_unique_alt; trivial. intros q. split. - split; trivial. now apply divide_mul_l. - now destruct 1. Qed.
imports: NZAxioms NZMulOrder