proposition: Lemma BQpair_real C: BQpair C -> real_dedekind (BQpairR C).
proof: Proof. move => [Ha Hb]. move:NS0 => ns0. move: (Ha) => [pa pb pc pd pe]. move:(pc _ NS0) => /setX_P [_ sa sb]. have ra: nonempty (BQpairR C). exists (Q (Vg C \0c)) => //;apply:Zo_i => //; exists \1c; fprops. by rewrite - succ_zero;apply: pe. have rb: BQpairR C <> BQ. have tx: inc (P (Vg C \0c)) (BQpairL C). by apply:Zo_i => //; exists \1c; fprops; rewrite - succ_zero;apply: pd. move => eq; move/(BQpair_aux2a_equiv2 Ha): Hb; rewrite eq => di. empty_tac1 (P (Vg C \0c)). have rc: forall x y, inc x (BQpairR C) -> x <q y -> inc y (BQpairR C). move => x y /Zo_P [_ [n na nb]] lxy; move:(proj32_1 lxy) => yq. apply:(Zo_i yq); exists n => //; BQo_tac. split => //;first by apply: Zo_S. move => x /Zo_P [xq [n na nb]]; move:(pe _ na) => nc. exists (Q (Vg C n)) => //; apply/Zo_P. rewrite -/(ratp _);split; [BQo_tac | exists (csucc n); fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)