proposition: Lemma MobiusZ x (p : {poly R}) : (size p <= deg.+1)%N -> Mobius deg a b (x *: p) = x *: Mobius deg a b p.
proof: Proof. move=> s; rewrite /Mobius /shift_poly /scaleX_poly /=. rewrite !linearZ recipZ; last first. rewrite /= !size_comp_poly2 //; first by rewrite size_XaddC. by rewrite size_XmulC // subr_eq0 eq_sym. by rewrite /= linearZ. 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