proposition: Lemma recipZ (q : {poly R}) c : (size q <= deg.+1)%N -> recip deg (c *: q) = c *: recip deg q.
proof: Proof. move=> s; rewrite !recipE // ?poly_def; last first. case h : (c == 0); first by rewrite (eqP h) scale0r size_poly0. by rewrite size_scale ?h. rewrite -[_ *: (\sum_(_ < _) _)]mul_polyC big_distrr; apply:eq_bigr. by move=> [i ci] _ /=; rewrite coefZ mul_polyC scalerA. 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