proposition: Lemma recip_scale_swap (q : {poly R}) c : c != 0 -> (size q <= deg.+1)%N -> recip deg (q \scale c) = (c ^+ deg)%:P * recip deg q \scale c^-1.
proof: Proof. move=> c0 sz; rewrite !recipE //; last by rewrite size_scaleX. rewrite !poly_def big_distrr /=. rewrite [_ \scale c^-1]/scaleX_poly linear_sum; apply: eq_bigr. move=> [i ci] _ /=; rewrite scaleX_polyE coef_poly. case h: (deg - i < size q)%N; last first. rewrite scale0r nth_default; last by rewrite leqNgt h. by rewrite scale0r mulr0 comp_poly0. rewrite comp_polyM comp_polyC comp_polyZ poly_comp_exp comp_polyX. rewrite (mulrC 'X) exprMn scalerAl -!mul_polyC -!polyC_exp mulrA -!polyCM. rewrite mulrA mulrAC [q`_ _ * _]mulrC; congr (_ %:P * _); congr (_ * _). case h' : (i < deg)%N; first by rewrite exprVn expfB. have -> : i = deg by apply/eqP; move: ci; rewrite ltnS leq_eqVlt h' orbF. by rewrite subnn expr0 exprVn mulfV // expf_neq0. 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