proposition: Lemma has_root_creal_size_gt1 (x : creal) (p : {poly F}) : (p != 0)%B -> p.[x] == 0 -> (1 < size p)%N.
proof: Proof. move=> p_neq0 rootpa. rewrite ltnNge leq_eqVlt ltnS leqn0 size_poly_eq0 (negPf p_neq0) orbF. apply/negP=> /size_poly1P [c c_neq0 eq_pc]; apply: rootpa. by rewrite eq_pc horner_cst_creal; apply/neq_creal_cst. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)