proposition: Lemma Bezout_pos_aux a b u v : intp a -> intp b -> b <> \0z -> Bezout_pos a b u v -> BZabs u <=z BZabs b.
proof: Proof. move => az bz anz [uz vzp ha hb]. move: (ZSo bz)(BZp_sBZ vzp) => nbz vz. move:(zle_triangular ZS1 (ZSp nbz vz)). have <-: a *z u = \1z +z (BZopp b) *z v. by rewrite - hb -(BZopp_prod_l bz vz);symmetry; apply:BZdiff_sum1; apply: ZSp. rewrite (BZprod_abs az uz) (BZprod_abs nbz vz) BZabs_opp BZabs_1 => le1. case: (equal_or_not (BZabs u) \0z) => eauz. rewrite eauz; apply/zle0xP; exact: (BZabs_iN bz). case: (equal_or_not v \0z) => evz. have: \1z <=z BZabs b. apply:BZ1_small; apply/BZps_iP;split; first by apply:(BZabs_iN bz). by move => hh;move:(BZabs_0p bz hh). move:hb;rewrite /Bezout_rel evz BZprod_0r (BZsum_0r (ZSp az uz)). by move /(BZprod_1_inversion_s az uz) => ->. have vsp: inc v BZps by apply/BZps_iP. move:(ZSa uz)(ZSa vz)(ZSa bz) => auz avz abz. apply/(BZprod_ple2r auz abz vsp); rewrite BZprodC. have h: inc (BZabs u) BZps by move/BZps_iP: (conj (BZabs_iN uz) eauz). move:(zlt_leT (BZprod_Mltgt0 h ha) le1); rewrite BZsumC. by move/(zlt_succ1P (ZSp vz auz) (ZSp abz avz)); rewrite (BZabs_pos vzp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)