proposition: Lemma lcm_mul_mono_l : forall n m p, lcm (p * n) (p * m) == p * lcm n m.
proof: Proof. intros n m p. destruct (eq_decidable p 0) as [Hp|Hp]. - rewrite Hp. nzsimpl. rewrite lcm_0_l. now nzsimpl. - destruct (eq_decidable (gcd n m) 0) as [Hg|Hg]. + 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 mul_assoc. f_equiv. now rewrite div_mul_cancel_l. Qed.
imports: NAxioms NSub NDiv NGcd