{q : Q | x < 'q < y}. Proof. assert (R : sig P). { apply minimal_n_alt_type. - apply QQpos_eq. - apply P_dec. - apply P_inhab. } unfold P in R. destruct R as [[q eps] [lleft mright]]. exists q; split. - nrefine (locates_right_false l _ lleft). - nrefine (locates_right_true m _ mright). Qed.
Require Import