proposition: Lemma lcm_mul_mono_l : forall n m p, lcm (p * n) (p * m) == abs p * lcm n m.
proof: Proof. intros n m p. destruct (eq_decidable p 0) as [Hp|Hp];[|destruct (eq_decidable (gcd n m) 0) as [Hg|Hg]]. - rewrite Hp. nzsimpl. rewrite lcm_0_l, abs_0. now nzsimpl. - apply gcd_eq_0 in Hg. destruct Hg as (Hn,Hm); rewrite Hn, Hm. nzsimpl. rewrite lcm_0_l. now nzsimpl. - unfold lcm. rewrite gcd_mul_mono_l. rewrite !abs_mul, mul_assoc. f_equiv. rewrite <- (abs_sgn p) at 1. rewrite <- mul_assoc. rewrite div_mul_cancel_l; trivial. + rewrite divide_div_mul_exact; trivial. * rewrite abs_mul. rewrite <- (sgn_abs (sgn p)), sgn_sgn. { destruct (sgn_spec p) as [(_,EQ)|[(EQ,_)|(_,EQ)]]. - rewrite EQ. now nzsimpl. - order. - rewrite EQ. rewrite mul_opp_l, mul_opp_r, opp_involutive. now nzsimpl. } * apply gcd_divide_r. + contradict Hp. now apply abs_0_iff. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor