proposition: Lemma Zgcd_plus_elim_rr : forall a b c : Z, Zdivides a c -> Zgcd a (b + c) = Zgcd a b.
proof: Proof. intros a b c Hdiv. elim (Zdec a). intro H0; rewrite H0; repeat rewrite Zgcd_zero_lft. replace c with 0%Z. rewrite Zplus_0_r; auto. rewrite H0 in Hdiv. symmetry in |- *. auto with zarith. intro Ha. apply Zdivides_antisymm. generalize (Zgcd_pos a (b + c)); auto with zarith. generalize (Zgcd_pos a b); auto with zarith. rewrite (Zgcd_lin_comb a b). apply Zdivides_plus_elim. apply Zdivides_mult_elim_lft. apply Zgcd_is_divisor_lft. apply Zdivides_mult_elim_lft. set (x := (b + c)%Z) in *; replace b with (b + c - c)%Z. unfold x in |- *. apply Zdivides_minus_elim. apply Zgcd_is_divisor_rht. apply (Zdivides_trans (Zgcd a (b + c)) a c). apply Zgcd_is_divisor_lft. assumption. lia. rewrite (Zgcd_lin_comb a (b + c)). apply Zdivides_plus_elim. apply Zdivides_mult_elim_lft. apply Zgcd_is_divisor_lft. apply Zdivides_mult_elim_lft. apply Zdivides_plus_elim. apply Zgcd_is_divisor_rht. apply (Zdivides_trans (Zgcd a b) a c). apply Zgcd_is_divisor_lft. assumption. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)