proposition: Lemma poly_size1 p : (size p <= 1)%N -> p = (p`_0)%:P.
proof: Proof. move=> sL. rewrite -[LHS]coefK poly_def; case E : size sL => [|[]]// _. by rewrite big_ord0 -[p]coefK E poly_def big_ord0 !coefC. by rewrite big_ord1 alg_polyC. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn