proposition: Lemma Qpairis_pr1P n k x: inc x (Qpairi k n) <-> (Qpair k n) <=q x /\ x <=q (Qpair (csucc k) n).
proof: Proof. split; first by move => /Zo_hi [/BQle_P ha /BQle_P hb ]. move => [/BQle_P pa /BQle_P pb]; apply: Zo_i => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)