proposition: Lemma Zgcd_minus_elim_rr : forall a b c : Z, Zdivides a c -> Zgcd a (b - c) = Zgcd a b.
proof: Proof. intros a b c Hdiv. unfold Zminus in |- *. apply Zgcd_plus_elim_rr. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)