proposition: Lemma Nbezout a b: natp a -> natp b -> a <> \0c -> Ncoprime a b -> exists u v, [/\ natp u, natp v, a *c u = \1c +c b *c v& (b <=c \1c \/ u <c b)].
proof: Proof. move: NS1 => n1 aN bN anz cp. case: (equal_or_not b \0c) => bnz. move:cp; rewrite /Ncoprime bnz (Ngcd_n0 aN) => ->. have aux: \0c <=c \1c \/ \1c <c \0c by left; exact:cle_01. by exists \1c, \1c; split => //; rewrite (cprod1r CS1) cprod0l(csum0r CS1). have bnz1: BZ_of_nat b <> \0z by move/BZ_of_nat_inj. move:(BZ_of_natp_i aN) (BZ_of_natp_i bN) => ap bp. move: (BZp_sBZ ap)(BZp_sBZ bp) => az bz. have cp':BZcoprime (BZ_of_nat b) (BZ_of_nat a). rewrite /BZcoprime BZgcd_C - (BZp_hi_pr (ZpS_gcd az bz)). by move: cp; rewrite /Ncoprime/Ngcd => ->. move: (Bezout_pos_exists bz az bnz1 cp') => [v [u [vz uzp us]]]. move:(BZ_valN (BZp_sBZ uzp)) (BZ_valN vz) => uN vN. move:(BZp_hi_pr uzp) => equ. rewrite /Bezout_rel -equ (BZprod_cN aN uN) => bb. have lc: b <=c \1c \/ P u <c b. by right; apply /(zlt_cN uN bN); rewrite equ - (BZabs_pos bp). case/BZ_i2P: (vz) => vp. move:bb; rewrite -(BZp_hi_pr (BZps_sBZp vp)) (BZprod_cN bN vN). rewrite (BZsum_cN (NS_prod bN vN)(NS_prod aN uN)). have ha:= (CS_prod2 a (P u)); have hb:= (CS_prod2 b (P v)). move/BZ_of_nat_inj => eq1. case:(csum_eq1 hb ha eq1) => eq2. exists (P u), (P v); split => //;rewrite - eq1 eq2 csum0l // csum0r//. move:eq1; rewrite eq2 (csum0r hb) => /(cprod_eq1 (CS_nat bN) (CS_nat vN)). move:(cpred_pr aN anz) => [sa sb] [b1 _]. have hc: b <=c \1c \/ \1c <c b by rewrite b1; left; fprops. exists \1c, (cpred a); split => //. by rewrite (cprod1r (CS_nat aN)) b1 (cprod1l (CS_nat sa)) csumC -Nsucc_rw. have ha:=(BZ_of_nat_i (NS_prod aN uN)). move:(BZopp_negative2 vp) => ovp. have: BZ_of_nat (a *c P u) = \1z -z BZ_of_nat b *z v. by rewrite - bb BZdiff_sum //; apply:ZSp. rewrite /BZdiff (BZopp_prod_r bz vz) -(BZp_hi_pr ovp) BZopp_val. rewrite (BZprod_cN bN vN) (BZsum_cN NS1 (NS_prod bN vN)); move/BZ_of_nat_inj. by move => h; exists (P u),(P v). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)