proposition: Lemma Zgcd_plus_elim_rl : forall a b c : Z, Zdivides a c -> Zgcd a (c + b) = Zgcd a b.
proof: Proof. intros a b c. rewrite Zplus_comm. apply Zgcd_plus_elim_rr. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)