proposition: Lemma left_right_polyE m p : (size p <= m.*2)%N -> p = left_poly m p + right_poly m p * 'X^m.
proof: Proof. move=> sL2m; apply/polyP => i. rewrite coefD coefMXn !coef_poly. case: leqP => HlP; last by rewrite addr0. case: leqP => H1lP; last by rewrite subnK ?add0r. rewrite add0r nth_default //. apply: leq_trans sL2m _. by rewrite -addnn -leq_subRL. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)