proposition: Lemma uniq_root_mu_seq (p : {poly F}) : uniq (root_seq p) -> forall x, x \in root_mu_seq p -> x.2 = 1%N.
proof: Proof. move=> H x /(nthP (0,0%N)) [] i; rewrite size_map=> Hi. rewrite (nth_map 0) // => <- /=; move: Hi. rewrite /root_seq_uniq undup_id // -count_root_seq => Hi. by rewrite count_uniq_mem // (mem_nth 0 Hi). Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)