proposition: Lemma size_root_seq p : size (root_seq p) = (size p).-1.
proof: Proof. have [-> | p0] := eqVneq p 0; first by rewrite root_seq0 size_poly0. rewrite {2}[p]root_seq_eq size_scale ?lead_coef_eq0 //. rewrite (big_nth 0) big_mkord size_prod. rewrite (eq_bigr (fun=> (1 + 1)%N)). by rewrite big_split sum1_card /= subSKn addnK card_ord. by move=> i _; rewrite size_XsubC. by move=> i _; rewrite polyXsubC_eq0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)