proposition: Lemma egcdp_recP : forall k p q, q != 0 -> size q <= k -> size q <= size p -> let e := (egcdp_rec p q k) in [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q].
proof: Proof. elim=> [|k ihk] p q /= qn0; first by rewrite size_poly_leq0 (negPf qn0). move=> sqSn qsp; rewrite (negPf qn0). have sp : size p > 0 by apply: leq_trans qsp; rewrite size_poly_gt0. have [r0 | rn0] /= := eqVneq (p %%q) 0. rewrite r0 /egcdp_rec; case: k ihk sqSn => [|n] ihn sqSn /=. rewrite !scaler0 !mul0r subr0 add0r mul1r size_poly0 size_poly1. by rewrite dvdp_gcd_idr /dvdp ?r0. rewrite !eqxx mul0r scaler0 /= mul0r add0r subr0 mul1r size_poly0 size_poly1. by rewrite dvdp_gcd_idr /dvdp ?r0 //. have h1 : size (p %% q) <= k. by rewrite -ltnS; apply: leq_trans sqSn; rewrite ltn_modp. have h2 : size (p %% q) <= size q by rewrite ltnW // ltn_modp. have := ihk q (p %% q) rn0 h1 h2. case: (egcdp_rec _ _)=> u v /= => [[ihn'1 ihn'2 ihn'3]]. rewrite gcdpE ltnNge qsp //= (eqp_ltrans (gcdpC _ _)); split; last first. - apply: (eqp_trans ihn'3). rewrite mulrBl addrCA -scalerAl scalerAr -mulrA -mulrBr. by rewrite divp_eq addrAC subrr add0r eqpxx. - apply: (leq_trans (size_add _ _)). have [-> | vn0] := eqVneq v 0. rewrite mul0r size_opp size_poly0 maxn0; apply: leq_trans ihn'1 _. exact: leq_modp. have [-> | qqn0] := eqVneq (p %/ q) 0. rewrite mulr0 size_opp size_poly0 maxn0; apply: leq_trans ihn'1 _. exact: leq_modp. rewrite geq_max (leq_trans ihn'1) ?leq_modp //= size_opp size_mul //. move: (ihn'2); rewrite (polySpred vn0) (polySpred qn0). rewrite -(ltn_add2r (size (p %/ q))) !addSn /= ltnS; move/leq_trans; apply. rewrite size_divp // addnBA ?addKn //. by apply: leq_trans qsp; apply: leq_pred. - by rewrite size_scale // lc_expn_scalp_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)