proposition: Lemma recipE (q : {poly R}) : (size q <= deg.+1)%N -> recip deg q = \poly_(i < deg.+1) q`_(deg - i).
proof: Proof. move=> sq. have t : forall n m (E : nat -> R), 'X ^+ n * \poly_(i < m) E i = \poly_(i < m + n) (E (i - n)%N *+ (n <= i)%N). elim=> [ | n IH] m E. rewrite expr0 mul1r addn0; rewrite !poly_def; apply: eq_bigr => i _. by rewrite subn0 leq0n mulr1n. rewrite exprS -mulrA IH !poly_def. rewrite addnS big_ord_recl. rewrite [X in _ *+ (n < X)]/nat_of_ord /= mulr0n scale0r add0r big_distrr. apply: eq_bigr; move=> [i ci] _ /=; rewrite /bump leq0n add1n ltnS subSS. by rewrite mulrC -scalerAl exprS mulrC. rewrite /recip t subnKC // !poly_def; apply: eq_bigr. move=> [i ci] _ /=; congr (_ *: _). case h : (deg.+1 - size q <= i)%N. rewrite mulr1n; congr (q`_ _); apply/eqP. rewrite -(eqn_add2r (i - (deg.+1 - size q)).+1) subnK; last first. by rewrite -(ltn_add2r (deg.+1 - size q)) subnK // addnC subnK. rewrite -subSn // addnBA; last by apply/(leq_trans h)/leqnSn. by rewrite addnS subnK // subKn. move/negP: h;move/negP; rewrite -ltnNge => h. rewrite mulr0n nth_default //. rewrite -(leq_add2r i.+1) -subSS subnK //. by rewrite addnC -(subnK sq) leq_add2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc