Definition minimal_n : ∑ n : nat, P n. Proof. induction prop_n_to_min_n as [n pl]. induction pl as [p _]. exact (n,,p). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.Propositions.