proposition: Lemma poly_size2 p : (size p <= 2)%N -> p = (p`_0)%:P + (p`_1)%:P * 'X.
proof: Proof. rewrite leq_eqVlt => /orP[/eqP spE|/poly_size1->]; last first. by rewrite !coefC /= mul0r addr0. by rewrite -[LHS]coefK poly_def spE big_ord_recr /= big_ord1 alg_polyC mul_polyC. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn