proposition: Lemma qle0xP x: \0q <=q x <-> inc x BQp.
proof: Proof. have H: ratp x -> (BQle_aux \0q x <-> inc x BQp). move => xQ; move:(xQ) => /BQ_P [_ nz dzp _]. rewrite /BQle_aux /BQ_zero /BQ_of_Z; aw; rewrite BZprod_0l (BZprod_1l nz). apply:(iff_trans (zle0xP _)). by split => h; [ apply: Zo_i | move/Zo_hi: h ]. split; first by move => [_ xq xp]; apply /(H xq). move => pa; move: (BQp_sBQ pa) => pb; split => //; first by apply: QS0. by apply/(H pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)