proposition: Lemma size_recip (q : {poly R}) : (size q <= deg.+1 -> size (recip deg q) <= deg.+1)%N.
proof: Proof. by move=> s; rewrite recipE // size_poly. 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