proposition: Lemma Zgcd_minus_elim_rl : forall a b c : Z, Zdivides a c -> Zgcd a (c - b) = Zgcd a b.
proof: Proof. intros a b c Hdiv. replace (c - b)%Z with (- (b - c))%Z. rewrite Zgcd_Zopp_r. apply Zgcd_minus_elim_rr. assumption. lia. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)