proposition: Lemma BQpair_aux2a_equiv2 C: BQpair_aux C -> (BQpair_aux2b C <->disjoint (BQpairL C)(BQpairR C)).
proof: Proof. move =>H; split. move => Ha. apply: disjoint_pr => u /Zo_P [uQ [n na nb]] /Zo_P [_ [m ma mb]]. by move: (proj2 (qlt_ltT (qlt_ltT nb (Ha _ _ na ma)) mb)). move => d; apply /(BQpair_aux2a_equiv H) => n nN. move: H => [pa pb pc pd pe]. move: (pc _ nN) => /setX_P[_ ha hb]. case: (qleT_el hb ha) => // le1. empty_tac1 (Q (Vg C n)). apply /Zo_P; split => //;exists (csucc n); fprops. move:(pd _ nN) => h; BQo_tac. apply /Zo_P; split => //; exists (csucc n); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)