proposition: Lemma recipK (q : {poly R}) : (size q <= deg.+1)%N -> recip deg (recip deg q) = q.
proof: Proof. move=> s; rewrite recipE; last by rewrite size_recip. rewrite -{2}[q]coefK (poly_extend s). apply: poly_ext => i c; rewrite recipE // coef_poly. rewrite subKn; last by rewrite -ltnS. by rewrite (leq_ltn_trans _ (ltnSn deg)) // leq_subr. by move=> i c; rewrite nth_default //; case/andP: c. 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