proposition: Lemma Bezout_pos_aux2 a b u v : intp a -> intp b -> b <> \0z -> BZabs b <> \1z -> Bezout_pos a b u v -> BZabs u <z BZabs b.
proof: Proof. move => az bz bnz abn1 ha; split; first apply: (Bezout_pos_aux az bz bnz ha). move: ha => [uz vzp ha hb] sa. have vz: intp v by BZo_tac. move:(ZS_sign u)(ZS_sign b) => su sb. have aux: inc (a *z BZsign u +z v *z BZsign b) BZ by apply:ZSs; apply: ZSp. move: hb; rewrite /Bezout_rel (BZabs_sign uz) (BZprodA az su (ZSa uz)). rewrite (BZprodC b) (BZabs_sign bz) (BZprodA vz sb (ZSa bz)) sa. have ra := ZSa bz. rewrite -BZprodDl //; try apply:ZSp => //. move /(BZprod_1_inversion_s aux (ZSa bz)). by rewrite BZabs_abs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)