proposition: Lemma left_poly_id m p : (size p <= m)%N -> left_poly m p = p.
proof: Proof. move=> Hs; apply/polyP => i. rewrite coef_poly; case: leqP => // Hs1. by apply/sym_equal/nth_default/(leq_trans Hs). Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)