proposition: Lemma Qpairis_pr2 k n: natp k -> natp n -> (inc (Qpair k n) (Qpairi k n) /\ inc (Qpair (csucc k) n) (Qpairi k n)).
proof: Proof. move=> kN xN; move: (NS_succ kN) => skN. have p5:(Qpair k n) <=q (Qpair (csucc k) n) by apply /Qpair_leP; fprops. move:(p5) =>[gha hb _]. have p3:(Qpair k n) <=q (Qpair k n) by apply: qleR. have p4:(Qpair (csucc k) n) <=q (Qpair (csucc k) n) by apply: qleR. by split; apply/Qpairis_pr1P. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)