proposition: Lemma qlt0xP x: \0q <q x <-> inc x BQps.
proof: Proof. split; first by move => [/qle0xP pa /nesym pb]; apply /BQps_iP. by move /BQps_iP => [/qle0xP h /nesym]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)