proposition: Lemma Bezout_pos_exists a b: intp a -> intp b -> a <> \0z -> BZcoprime a b -> exists u v, Bezout_pos a b u v.
proof: Proof. move => az bz anz /(BZ_Bezout_if_coprime az bz) [u [v [uz vz h]]]. move:(BZdvd_correct vz az anz) => [qz rp [sc sd /BZp_sBZ rz]]. have ha: inc ((v %/z a) *z b) BZ by apply:ZSp. have hb:inc (u +z (v %/z a) *z b) BZ by apply: ZSs. move: h; rewrite /Bezout_rel sc (BZprodDr bz (ZSp az qz) rz) (BZprodC b). rewrite - (BZprodA az qz bz) (BZsumA (ZSp az uz) (ZSp az ha) (ZSp bz rz)). rewrite - (BZprodDr az uz ha) => hh. by exists (u +z (v %/z a) *z b), (v %%z a). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)