proposition: Lemma Zgcd_lin : forall a b c, (Z.abs c * Zgcd a b = Zgcd (c * a) (c * b))%Z.
proof: Proof. intros a b c. case (Z.eq_dec a 0). intro H; rewrite H; rewrite Zmult_0_r, Zgcd_zero_lft, Zgcd_zero_lft; apply Zabs_mult_compat. intro Ha; case (Z.eq_dec b 0). intro H; rewrite H; rewrite Zmult_0_r, Zgcd_zero_rht, Zgcd_zero_rht; apply Zabs_mult_compat. intro Hb; case (Z.eq_dec c 0). intro H; rewrite H; rewrite Zmult_0_l, Zmult_0_l, Zmult_0_l, Zgcd_zero_lft; reflexivity. intro Hc; apply Zdivides_antisymm. rewrite <- (Zmult_0_r (Z.abs c)). apply Zmult_pos_mon_lt_lft. apply Z.lt_gt. apply Zgcd_pos. left; assumption. destruct c; [destruct Hc| |]; reflexivity. apply Z.lt_gt. apply Zgcd_pos. left. intro H0; destruct (Zmult_zero_div _ _ H0). destruct Hc; assumption. destruct Ha; assumption. apply Zdiv_gcd_elim. apply Zdivides_mult_elim. apply Zdivides_abs_elim_lft. apply Zdivides_ref. apply Zgcd_is_divisor_lft. apply Zdivides_mult_elim. apply Zdivides_abs_elim_lft. apply Zdivides_ref. apply Zgcd_is_divisor_rht. cut (forall c : positive, Zdivides (Zgcd (c * a) (c * b)) (Z.abs c * Zgcd a b)). intro H; case c. simpl; rewrite Zgcd_zero_lft; apply Zdivides_ref. apply H. intro p; rewrite Zgcd_abs. rewrite <- Zabs_mult_compat, <- Zabs_mult_compat. simpl (Z.abs (Zneg p)). assert ((p:Z) = Z.abs p). reflexivity. rewrite H0; clear H0. rewrite Zabs_mult_compat, Zabs_mult_compat. rewrite <- Zgcd_abs. apply H. clear c Hc; intro c. rewrite (Zgcd_lin_comb a b). rewrite Zmult_plus_distr_r. simpl (Z.abs c). rewrite Zmult_assoc, Zmult_assoc. rewrite (Zmult_comm c (Zgcd_coeff_a a b)). rewrite (Zmult_comm c (Zgcd_coeff_b a b)). rewrite <- Zmult_assoc, <- Zmult_assoc. apply Zdivides_plus_elim. apply Zdivides_mult_elim_lft. apply Zgcd_is_divisor_lft. apply Zdivides_mult_elim_lft. apply Zgcd_is_divisor_rht. Qed.
imports: CRings Zring