proposition: Lemma qge0xP x: x <=q \0q <-> inc x BQm.
proof: Proof. have H: ratp x -> (BQle_aux x \0q <-> inc x BQm). move => xQ; move:(xQ) => /BQ_P [_ nz dzp _]. rewrite /BQle_aux /BQ_zero /BQ_of_Z; aw; rewrite BZprod_0r (BZprod_1r nz). apply:(iff_trans (zge0xP _)). by split => h; [ apply: Zo_i | move/Zo_hi: h ]. split; first by move => [xz _ x0]; apply /(H xz). move => pa; move: (BQm_sBQ pa) => pb; split => //; first by apply: QS0. by apply/(H pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)