proposition: Lemma root_root_mu_seq p : [seq x.1 | x <- root_mu_seq p] = root_seq_uniq p.
proof: Proof. apply: (@eq_from_nth _ 0)=>[|i]; rewrite !size_map //. by move=> Hi; rewrite (nth_map (0,0%N)) ?size_map // (nth_map 0) //. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)