proposition: Lemma recompose_split : forall n b p, size p <= b * n -> (split_poly n b p).['X^b] = p.
proof: Proof. rewrite /split_poly => [[b p|n b p hs]]; rewrite horner_poly ?big_ord_recr /=. by rewrite muln0 leqn0 size_poly_eq0 => /eqP ->; rewrite big_ord0. suff -> : \big[+%R/0]_(i < n) (\poly_(j < b) p`_(i * b + j) * 'X^b ^+ i) = \poly_(i < n * b) p`_i. apply/polyP=> i; rewrite -exprM coefD coefMXn coef_poly mulnC. have [_|hbni] := ltnP; rewrite ?addr0 // add0r coef_poly. have [_|hsub] := ltnP; rewrite ?subnKC // ?nth_default //. rewrite -ltnS -subSn // ltn_subRL ltnS addnC -mulnS in hsub. exact: (leq_trans hs hsub). elim: n {hs} => [|n ih]; first by rewrite mul0n poly_def !big_ord0. apply/polyP=> i. rewrite big_ord_recr /= ih -exprM coefD !coef_poly coefMXn mulSn mulnC. have [h1|hbni] := ltnP; first by rewrite addr0 (ltn_addl b h1). by rewrite add0r coef_poly subnKC // -(ltn_add2r (b * n)) subnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple) mathcomp(finfun bigop fingroup perm ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly)