proposition: Lemma finite_dec_exists: forall (X:Type) (P:X->Prop), FiniteT X -> (forall x:X, P x \/ ~ P x) -> (exists x:X, P x) \/ (forall x:X, ~ P x).
proof: Proof. intros. revert P H0. induction H. - right. destruct x. - intros. case (IHFiniteT (fun x:T => P (Some x)) (fun x:T => H0 (Some x))). + left. destruct H1 as [x]. exists (Some x). assumption. + intro. specialize (H0 None) as [|]. * left. exists None. assumption. * right. destruct x. -- apply H1. -- assumption. - destruct H0. intros. specialize (IHFiniteT (fun x:X => P (f x)) (fun x:X => H2 (f x))) as [|]. * left. destruct H3 as [x]. exists (f x). assumption. * right. intro. rewrite <- H1 with x. apply H3. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)