proposition: Theorem representative_boolean_partition_imp_excluded_middle : representative_boolean_partition -> excluded_middle.
proof: Proof. intros ReprFunChoice P. pose (R (b1 b2 : bool) := b1 = b2 \/ P). assert (Equivalence R). { split. - now left. - destruct 1. + now left. + now right. - destruct 1, 1; try now right. left; now transitivity y. } destruct (ReprFunChoice R H) as (f,Hf). clear H. destruct (Bool.bool_dec (f true) (f false)) as [Heq|Hneq]. + left. destruct (Hf false) as ([Hfalse|HP],_); try easy. destruct (Hf true) as ([Htrue|HP],_); try easy. congruence. + right. intro HP. destruct (Hf true) as (_,H). apply Hneq, H. now right. Qed.
imports: PropExtensionalityFacts Hurkens Coq.Arith.PeanoNat Wf_nat RelationClasses