proposition: Lemma MobiusK (q : {poly R}) : (size q <= deg.+1)%N -> Mobius deg a b (relocate q) = (b-a) ^+deg *: q.
proof: Proof. move=> s; rewrite /relocate /Mobius ltnNge s /= /shift_poly. rewrite -[X in (_ \Po (_ + _)) \Po (_ + X%:P)]opprK [(- - _)%:P]polyCN. have ba : b - a != 0 by rewrite subr_eq0 eq_sym. have bav : (b - a)^-1 != 0 by rewrite invr_eq0. have s1 : (size (q \Po ('X + (-1)%:P)) <= deg.+1)%N. by rewrite size_comp_poly2 // size_XaddC. have rr : GRing.rreg ((b - a) ^+ deg). by rewrite /GRing.rreg; apply: mulIf; rewrite expf_eq0 (negbTE ba) andbF. rewrite comp_polyXaddC_K !recip_scale_swap //; last first. by rewrite size_scaleX // mulrC rreg_size ?size_recip. by rewrite mulrC rreg_size ?size_recip. rewrite !mul_polyC recipZ; last first. by apply: size_recip; rewrite size_comp_poly2 // size_XaddC. rewrite !scalerA exprVn mulVf ?scale1r; last first. by rewrite expf_eq0 (negbTE ba) andbF. rewrite invrK recipK; last by rewrite size_comp_poly2 // size_XaddC. rewrite !scaleZ scaleS mulfV // scalep1 linearZ /=. rewrite -[X in (_ \Po _) \Po (_ + X%:P)]opprK (polyCN (-1)). by rewrite comp_polyXaddC_K. 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