proposition: Lemma ch_min_proof : has_unique_least_element le P.
proof: Proof. apply dec_inh_nat_subset_has_unique_least_element; auto. intros. apply classic. Qed.
imports: Coq(Classical_Prop IndefiniteDescription Wf_nat Relations)