proposition: Lemma Mk_Cexists R k s : classically (exists M : {set 'Z_k}, Mk_spec R s M).
proof: Proof. rewrite /Mk_spec. suff : classically (exists M : {set 'Z_k}, forall x : 'Z_k, x \in (enum 'Z_k) -> uniq (enum 'Z_k) -> is_iexpm_spec R 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 nat (fun m => (a = m %% k :> nat)%N /\ is_iexp R k s m). 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_iexpm_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_iexpm_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