proposition: Theorem excluded_middle_entails_unrestricted_minimization : forall P, Minimization_Property P.
proof: Proof. intros P n HPn. assert (dec : forall n, P n \/ ~ P n) by auto using em. assert (ex : exists n, P n) by (exists n; assumption). destruct (dec_inh_nat_subset_has_unique_least_element P dec ex) as (n' & HPn' & _). exists n'. assumption. Qed.
imports: PropExtensionalityFacts Hurkens Coq.Arith.PeanoNat Wf_nat