proposition: Lemma BQpair_single3 C: BQpair_aux2b C -> (BQpair_aux3 C <-> exists t, [/\ ratp t, forall x, x <q t -> exists2 n, natp n & x <q P (Vg C n) & forall x, t <q x -> exists2 n, natp n & Q (Vg C n) <q x ]).
proof: Proof. move => Hb; split. move => [t tp]; exists t. have aux: forall x, ratp x -> x <> t -> (inc x (BQpairL C) \/ inc x (BQpairR C)). move => x xq /set1_P ; rewrite - tp => /setC_P h; ex_middle hh. by case h; split => // /setU2_P. move: (set1_1 t); rewrite - tp => /setC_P [tq tv]; split => // x lxt. case:(aux x (proj31_1 lxt) (proj2 lxt)) => /Zo_P [xq [m ma mb]]. by exists m. case: tv; apply /setU2_P; right; apply:Zo_i => //; exists m => //; BQo_tac. case:(aux x (proj32_1 lxt) (nesym (proj2 lxt))) => /Zo_P [xq [m ma mb]]. case: tv; apply /setU2_P;left; apply:Zo_i => //; exists m => //; BQo_tac. by exists m. move => [t [tq ha hb]]; exists t; apply:set1_pr. apply/setC_P; split => // /setU2_P; case => /Zo_P [_ [n na nb]]. move: (hb _ nb) => [m mN hc]; move: (Hb n m na mN) => [nc _]; BQo_tac. move: (ha _ nb) => [m mN hc]; move: (Hb _ _ mN na) => [nc _];BQo_tac. move => z /setC_P [za /setU2_P zu]; case (qleT_ell za tq) => //. by move => /ha [n na nb]; case: zu; left; apply:Zo_i => //; exists n. by move => /hb [n na nb]; case: zu; right; apply:Zo_i => //; exists n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)