proposition: Lemma normal_size_le1 (p : {poly R}) : p \is normal -> (size p <= 1%N)%N = (size p == 1%N)%N.
proof: Proof. move=> Hpnormal. rewrite eqn_leq. apply/idP/idP => [Hpsize | /andP Hpsize]. apply/andP; split => //. by rewrite ltnNge leqn0 size_poly_eq0 normal_neq0. exact: (proj1 Hpsize). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)