proposition: Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 -> (gcd n m == 1 <-> lcm n m == abs (n*m)).
proof: Proof. intros n m Hn Hm. split; intros H. - unfold lcm. rewrite H. now rewrite div_1_r. - unfold lcm in *. rewrite !abs_mul in H. apply mul_cancel_l in H; [|now rewrite abs_0_iff]. assert (H' := gcd_divide_r n m). assert (Hg : gcd n m ~= 0) by (red; rewrite gcd_eq_0; destruct 1; order). apply mod_divide in H'; trivial. apply div_exact in H'; trivial. assert (m / gcd n m ~=0) by (contradict Hm; rewrite H', Hm; now nzsimpl). rewrite <- (mul_1_l (abs (_/_))) in H. rewrite H' in H at 3. rewrite abs_mul in H. apply mul_cancel_r in H; [|now rewrite abs_0_iff]. rewrite abs_eq in H. { order. } apply gcd_nonneg. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor