{q : Q | ' q < x}. Proof. assert (qP_lower : {q : Q | P_lower q}) by refine (minimal_n_alt_type Q Q_eq P_lower _ P_lower_inhab). destruct qP_lower as [q Pq]. exists (q - 1). unfold P_lower in Pq. simpl in *. apply (un_inl _ Pq). Qed.
Require Import