proposition: Lemma relocate0 (p : {poly R}) : (size p <= deg.+1)%N -> (relocate p == 0) = (p == 0).
proof: Proof. move=> s; apply/idP/idP; last first. move/eqP=> ->; rewrite /relocate /shift_poly /scaleX_poly !linear0. by rewrite size_poly0 ltn0 recip0 linear0. have bmax : (b - a) ^+ deg != 0 by rewrite expf_neq0 // subr_eq0 eq_sym. move/eqP=> r0; rewrite -[p]mul1r -[1]/1%:P -(mulVf bmax) polyCM -mulrA. rewrite !mul_polyC -MobiusK // r0 /Mobius /shift_poly /scaleX_poly !linear0. by rewrite recip0 linear0 scaler0. 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