proposition: Lemma Qh_Cexists (R : finRingType) k s (h : {poly R}) : classically (exists M : {set {poly %/ h}}, Qh_spec k s M).
proof: Proof. rewrite /Qh_spec. suff : classically (exists M : {set {poly %/ h}}, forall x : {poly %/ h}, x \in (enum {poly %/ h}) -> uniq (enum {poly %/ h}) -> is_iexph_spec k s x (x \in M)). apply: classic_bind => [[M HM]]. apply/classicP=> [] []; exists M => x. apply: HM; first by rewrite mem_enum inE. by apply: enum_uniq. elim: (enum _) => [|a l] //. by apply/classicP=> [] []; exists setT=> x; rewrite inE. apply: classic_bind => [[M HM]]. have /classic_bind := @classic_pick _ (fun p : {poly R} => a = in_qpoly h p /\ is_ipoly k s p). apply => [] [[ma [maE maI]]|Ha]. apply/classicP => [] []; exists (a |: M) => x. rewrite !inE => /orP[/eqP-> /= /andP[aNIi Ul]|xIl /= /andP[aNIl Ul]]. by rewrite eqxx; apply: is_iexph_spec_true maI. case: eqP => [xE|_ /=]; first by case/negP: aNIl; rewrite -xE. by apply: HM. apply/classicP => [] []; exists (M :\ a) => x. rewrite !inE => /orP[/eqP-> /= /andP[aNIi Ul]|xIl /= /andP[aNIl Ul]]. rewrite eqxx; apply: is_iexph_spec_false=> m Hm. by apply/eqP=> eE; case: (Ha m). rewrite (_ : x != a); first by by apply: HM. by apply: contra aNIl => /eqP<-. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound