proposition: Lemma size_linear_factor_leq1 p : forall q, q \in linear_factor_seq p -> (1 < size q)%N.
proof: Proof. move=> q; have [-> | Hp Hq] := eqVneq p 0. rewrite /linear_factor_seq /root_mu_seq. by rewrite /root_seq_uniq /root_seq size_poly0. rewrite -(nth_index 0 Hq) (nth_map (0,0%N)); last first. by rewrite -index_mem size_map in Hq. rewrite size_exp_XsubC (nth_map 0); last first. by rewrite -index_mem !size_map in Hq. rewrite -(@prednK (\mu_ _ _)) // mu_gt0 // -root_root_seq //. rewrite -mem_undup mem_nth //. by rewrite -index_mem !size_map in Hq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)