proposition: Lemma Zgcd_nat_divides (a b: Z): exists c: Z, (c * Zgcd_nat a b = a)%Z.
proof: Proof. Proof with auto. intros. unfold Zgcd_nat. pose proof (Zgcd_nonneg a b) as E. destruct (Zgcd_is_divisor a b) as [c ?]. exists c. destruct (Zgcd a b)... rewrite inject_nat_convert... exfalso. apply E. reflexivity. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)