proposition: Lemma gcd_mul_mono_l : forall n m p, gcd (p * n) (p * m) == p * gcd n m.
proof: Proof. intros n m p. apply gcd_unique. - apply mul_divide_mono_l, gcd_divide_l. - apply mul_divide_mono_l, gcd_divide_r. - intros q H H'. destruct (eq_0_gt_0_cases n) as [EQ|LT]. + rewrite EQ in *. now rewrite gcd_0_l. + destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial. apply divide_add_cancel_r with (p*m*b). * now apply divide_mul_l. * rewrite <- mul_assoc, <- mul_add_distr_l, add_comm, (mul_comm m), <- EQ. rewrite (mul_comm a), mul_assoc. now apply divide_mul_l. Qed.
imports: NAxioms NSub NZGcd