proposition: Lemma BQ_i2P x: ratp x <-> (inc x BQps \/ inc x BQm).
proof: Proof. split; last by case => h; [apply: BQps_sBQ | apply: BQm_sBQ]. move => h; move /BQ_P: (h) => [_ /BZ_i2P ha _ _]. by case:ha; [left | right];apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)