proposition: Lemma size_poly_eq1 p : (size p == 1) = (p %= 1).
proof: Proof. apply/size_poly1P/idP=> [[c cn0 ep] |]. by apply/eqpP; exists (1, c); rewrite ?oner_eq0 // alg_polyC scale1r. by move/eqp_size; rewrite size_poly1; move/eqP/size_poly1P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)