{r : Q | x < ' r}. Proof. assert (rP_upper : {r : Q | P_upper r}) by refine (minimal_n_alt_type Q Q_eq P_upper _ P_upper_inhab). destruct rP_upper as [r Pr]. exists (r + 1). unfold P_upper in Pr. simpl in *. destruct (l r (r + 1) (lt1N r)). - simpl in Pr. destruct (Pr tt). - assumption. Qed.
Require Import