proposition: Lemma Bezout_coprimepPn p q : p != 0 -> q != 0 -> reflect (exists2 uv : {poly R} * {poly R}, (0 < size uv.1 < size q) && (0 < size uv.2 < size p) & uv.1 * p = uv.2 * q) (~~ (coprimep p q)).
proof: Proof. move=> pn0 qn0; apply: (iffP idP); last first. case=> [[u v] /= /andP [/andP [ps1 s1] /andP [ps2 s2]] e]. have: ~~(size (q * p) <= size (u * p)). rewrite -ltnNge !size_mul // -?size_poly_gt0 // (polySpred pn0) !addnS. by rewrite ltn_add2r. apply: contra => ?; apply: dvdp_leq; rewrite ?mulf_neq0 // -?size_poly_gt0 //. by rewrite mulrC Gauss_dvdp // dvdp_mull // e dvdp_mull. rewrite coprimep_def neq_ltn ltnS size_poly_leq0 gcdp_eq0. rewrite (negPf pn0) (negPf qn0) /=. case sg: (size (gcdp p q)) => [|n] //; case: n sg=> [|n] // sg _. move: (dvdp_gcdl p q); rewrite dvdp_eq; set c1 := _ ^+ _; move/eqP=> hu1. move: (dvdp_gcdr p q); rewrite dvdp_eq; set c2 := _ ^+ _; move/eqP=> hv1. exists (c1 *: (q %/ gcdp p q), c2 *: (p %/ gcdp p q)); last first. by rewrite -!scalerAl !scalerAr hu1 hv1 mulrCA. rewrite !size_scale ?lc_expn_scalp_neq0 //= !size_poly_gt0 !divp_eq0. rewrite gcdp_eq0 !(negPf pn0) !(negPf qn0) /= -!leqNgt leq_gcdpl //. rewrite leq_gcdpr //= !ltn_divpl -?size_poly_eq0 ?sg //. rewrite !size_mul // -?size_poly_eq0 ?sg // ![(_ + n.+2)%N]addnS /=. by rewrite -!(addn1 (size _)) !leq_add2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)