proposition: Lemma BQ_i1P x: ratp x <-> [\/ x = \0q, inc x BQps | inc x BQms].
proof: Proof. split. move => h; move /BQ_P: (h) => [_ /BZ_i1P ha _ _]; case: ha => t. + by constructor 1; apply:BQnum0_P. + by constructor 2; apply:Zo_i. + by constructor 3; apply:Zo_i. by case; [move => ->; apply: QS0 | apply: BQps_sBQ | apply: BQms_sBQ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)