proposition: Lemma Zrelprime_mult_elim_lft : forall a b c : Z, Zrelprime a c -> Zrelprime b c -> Zrelprime (a * b) c.
proof: Proof. intros a b c. unfold Zrelprime in |- *. intros Ha Hb. generalize (Zgcd_lin_comb a c); rewrite Ha; set (p := Zgcd_coeff_a a c) in *; set (q := Zgcd_coeff_b a c) in *. generalize (Zgcd_lin_comb b c); rewrite Hb; set (r := Zgcd_coeff_a b c) in *; set (s := Zgcd_coeff_b b c) in *. intros Hla Hlb. apply Zdivides_antisymm. apply Z.lt_gt; apply Zgcd_pos. case (Zdec c); auto. intro Hc0. left. rewrite Hc0 in Ha; rewrite Zgcd_zero_rht in Ha; rewrite Hc0 in Hb; rewrite Zgcd_zero_rht in Hb; intro Hfalse. generalize (Zmult_zero_div _ _ Hfalse); intro H0; elim H0. intro Ha0; rewrite Ha0 in Ha; discriminate. intro Hb0; rewrite Hb0 in Hb; discriminate. auto with zarith. replace 1%Z with ((r * b + s * c) * (p * a + q * c))%Z. repeat rewrite Zmult_plus_distr_r; repeat rewrite Zmult_plus_distr_l; rewrite (Zmult_comm p a); rewrite (Zmult_comm a b); apply Zdivides_plus_elim; apply Zdivides_plus_elim; auto with zarith. rewrite <- Hla; rewrite <- Hlb; auto with zarith. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)