proposition: Lemma Zrelprime_gcd_mult_elim_lft : forall a b c : Z, Zrelprime a b -> Zgcd (a * b) c = (Zgcd a c * Zgcd b c)%Z.
proof: Proof. intros a b c. unfold Zrelprime in |- *. case (Zdec (a * b)). intro Hab0. generalize (Zmult_zero_div a b Hab0); intro Hab. elim Hab; intro H1; rewrite Hab0; rewrite H1; repeat rewrite Zgcd_zero_lft; repeat rewrite Zgcd_zero_rht; intro H2; rewrite Zgcd_abs; rewrite H2; rewrite Zgcd_one_lft; auto with zarith. intros Hab0 Hrelprime. apply Zdivides_antisymm. apply Z.lt_gt; apply Zgcd_pos; auto. rewrite <- (Zmult_0_r (Zgcd a c)). apply Zmult_pos_mon_lt_lft. apply Z.lt_gt; apply Zgcd_pos; left; rewrite Zmult_comm in Hab0; auto with zarith. apply Z.lt_gt; apply Zgcd_pos; left; auto with zarith. rewrite (Zgcd_lin_comb a c); rewrite (Zgcd_lin_comb b c). repeat rewrite Zmult_plus_distr_r; repeat rewrite Zmult_plus_distr_l. apply Zdivides_plus_elim; apply Zdivides_plus_elim; auto with zarith. apply Zdiv_gcd_elim. apply Zdivides_mult_elim; auto with zarith. apply Zrelprime_div_mult_elim; auto with zarith. apply (Zrelprime_divides_intro (Zgcd a c) (Zgcd b c) a b); auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)