proposition: Lemma BQ_i0P x: ratp x <-> (inc x BQms \/ inc x BQp).
proof: Proof. split; last by case => h; [ apply: BQms_sBQ | apply: BQp_sBQ]. move => xq; move /BQ_P: (xq) => [_ /BZ_i0P ha _ _]. by case:ha; [left | right];apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)