proposition: Lemma Zgcd_intro : forall a b d : Z, Zis_gcd a b d -> Zgcd a b = d.
proof: Proof. intros a b d Hisgcd. apply (Zis_gcd_unique a b (Zgcd a b) d). apply Zgcd_is_gcd. exact Hisgcd. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)