proposition: Lemma Zrelprime_div_mult_intro : forall a b c : Z, Zrelprime a b -> Zdivides a (b * c) -> Zdivides a c.
proof: Proof. intros a b c Hab Hdiv. case (Zdec (Z.abs a - 1)). intro H1. exists (c * Z.sgn a)%Z. rewrite <- Zmult_assoc. replace (Z.sgn a * a)%Z with (Z.abs a) by auto with zarith. replace (Z.abs a) with 1%Z; auto with zarith. intro Hn1. unfold Zrelprime in Hab. generalize (Zgcd_lin_comb a b). rewrite Hab. set (u := Zgcd_coeff_a a b); set (v := Zgcd_coeff_b a b). intro H1. replace c with (u * a * c + v * b * c)%Z. apply Zdivides_plus_elim. auto with zarith. rewrite <- Zmult_assoc. auto with zarith. symmetry in |- *. rewrite <- (Zmult_1_l c). replace (u * a * (1 * c))%Z with (u * a * c)%Z. replace (v * b * (1 * c))%Z with (v * b * c)%Z. rewrite H1. auto with zarith. rewrite Zmult_1_l; auto. rewrite Zmult_1_l; auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)