proposition: Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 -> (gcd n m == 1 <-> lcm n m == n*m).
proof: Proof. intros n m Hn Hm. split; intros H. - unfold lcm. rewrite H. now rewrite div_1_r. - unfold lcm in *. apply mul_cancel_l in H; trivial. assert (Hg : gcd n m ~= 0) by (red; rewrite gcd_eq_0; destruct 1; order). assert (H' := gcd_divide_r n m). apply mod_divide in H'; trivial. apply div_exact in H'; trivial. rewrite H in H'. rewrite <- (mul_1_l m) in H' at 1. now apply mul_cancel_r in H'. Qed.
imports: NAxioms NSub NDiv NGcd