{ n : nat & P n }. Proof. destruct prop_n_to_min_n as [n pl]. destruct pl as [p _]. exact (n; fst merely_inhabited_iff_inhabited_stable p). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Truncations.Core. Require Import HoTT.Spaces.Nat.Core.