proposition: Lemma relocateK (q : {poly R}) : (size q <= deg.+1)%N -> relocate (Mobius deg a b q) = (b-a) ^+deg *: q.
proof: Proof. move=> s; rewrite /relocate /Mobius. rewrite size_comp_poly2; last by rewrite size_XaddC. set sc := ((q \shift _) \scale _). set sz := size _. have dif : b - a != 0 by rewrite subr_eq0 eq_sym. have t : (size sc <= deg.+1)%N. by rewrite size_scaleX // size_comp_poly2 //; apply: size_XaddC. have t' : (sz <= deg.+1)%N by apply: size_recip. rewrite ltnNge t' /= -shift_polyD addNr. rewrite [_ \shift 0]/shift_poly addr0 comp_polyXr. rewrite recip_scale_swap // recipK // /sc mul_polyC /scaleX_poly linearZ /=. rewrite -comp_polyA comp_polyM comp_polyX comp_polyC -mulrA -polyCM. by rewrite mulVf // mulr1 comp_polyXr linearZ /= shift_polyDK. 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