proposition: Lemma Zis_gcd_bezout : forall a b d:Z, Zis_gcd a b d -> Bezout a b d.
proof: Proof. intros a b d Hgcd. case (extgcd a b) as [[u v] g] eqn:E, (extgcd_correct _ _ E) as [G ?Hg]. destruct (Zis_gcd_uniqueness_apart_sign a b d g Hgcd ltac:(rewrite Hg; apply Zgcd_is_gcd)); subst; (apply Bezout_intro with u v + apply Bezout_intro with (- u) (- v)); ring. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat