proposition: Lemma is_min_ch : forall n, P n -> proj1_sig ch_min <= n.
proof: Proof. destruct (proj2_sig ch_min) as [H _]. destruct H. intros. apply H0. auto. Qed.
imports: Coq(Classical_Prop IndefiniteDescription Wf_nat Relations)