proposition: Lemma gcd_mul_mono_l : forall n m p, gcd (p * n) (p * m) == abs p * gcd n m.
proof: Proof. intros n m p. apply gcd_unique. - apply mul_nonneg_nonneg; trivial using gcd_nonneg, abs_nonneg. - destruct (gcd_divide_l n m) as (q,Hq). rewrite Hq at 2. rewrite mul_assoc. apply mul_divide_mono_r. rewrite <- (abs_sgn p) at 2. rewrite <- mul_assoc. apply divide_factor_l. - destruct (gcd_divide_r n m) as (q,Hq). rewrite Hq at 2. rewrite mul_assoc. apply mul_divide_mono_r. rewrite <- (abs_sgn p) at 2. rewrite <- mul_assoc. apply divide_factor_l. - intros q H H'. destruct (gcd_bezout n m (gcd n m) (eq_refl _)) as (a & b & EQ). rewrite <- EQ, <- sgn_abs, mul_add_distr_l. apply divide_add_r. + rewrite mul_shuffle2. now apply divide_mul_l. + rewrite mul_shuffle2. now apply divide_mul_l. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd