proposition: Theorem classical_definite_description : forall (A : Type) (P : A->Prop), inhabited A -> { x : A | (exists! x : A, P x) -> P x }.
proof: Proof. intros A P i. destruct (excluded_middle_informative (exists! x, P x)) as [Hex|HnonP]. - apply constructive_definite_description with (P:= fun x => (exists! x : A, P x) -> P x). destruct Hex as (x,(Hx,Huni)). exists x; split. + intros _; exact Hx. + firstorder. - exists i; tauto. Qed.
imports: Classical Description ChoiceFacts