proposition: Lemma Zgcd_rec : forall a b : Z, b <> 0%Z -> Zgcd a b = Zgcd b (Z.abs a mod Z.abs b).
proof: Proof. intros a b Hb. unfold Zgcd in |- *. rewrite Zgcd_duv_rec. elim (Zgcd_duv b (Z.abs a mod Z.abs b)); intros d uv; elim uv; intros u v. reflexivity. exact Hb. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)