proposition: Lemma root_mu_seq_pos x p : p != 0 -> x \in root_mu_seq p -> (0 < x.2)%N.
proof: Proof. move=> Hp H. have Hr: size (root_seq_uniq p) = size (root_mu_seq p) by rewrite size_map. have Hs: (index x (root_mu_seq p) < size (root_seq_uniq p))%N. by rewrite Hr index_mem. rewrite -(nth_index (0,0%N) H) // (nth_map 0) // mu_gt0 //. by rewrite -root_root_seq // -mem_undup mem_nth. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)