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. apply exclusive_dec. red; intro. destruct H0. destruct H0. contradiction (H1 x). revert P X0. induction H. right. destruct x. intros. case (IHFiniteT (fun x:T => P (Some x)) (fun x:T => X0 (Some x))). left. destruct H0. exists (Some x). assumption. intro. case (X0 None). left. exists None. assumption. right. destruct x. apply H0. assumption. destruct H0. intros. case (IHFiniteT (fun x:X => P (f x)) (fun x:X => X0 (f x))). left. destruct H2. exists (f x). assumption. right. intro. rewrite <- H1 with x. apply H2. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description