proposition: Lemma uniq_root_dvdp p q : q != 0 -> (uniq (root_seq q)) -> p %| q -> (uniq (root_seq p)).
proof: Proof. move=> Hq Hq2 Hpq. apply: count_mem_uniq=> x. have Hc:= count_uniq_mem x Hq2. have Hle: (count_mem x (root_seq p) <= count_mem x (root_seq q))%N. rewrite !count_root_seq; case/dvdpP: Hpq => r Hr. by rewrite Hr mu_mul -?Hr // leq_addl. have: (count_mem x (root_seq p) <= 1)%N. by rewrite (leq_trans Hle) // Hc; case: (x \in root_seq q). rewrite leq_eqVlt ltnS leqn0. case Hp: (x \in root_seq p). rewrite -has_pred1 has_count in Hp. by rewrite (eqn_leq _ 0%N) leqNgt Hp orbF => /eqP ->. by rewrite eqn_leq -has_count has_pred1 Hp andbF orFb => /eqP ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)