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