proposition: Lemma Qpairis_prP x: inc x Qpairis <-> exists k n, [/\ natp k, natp n & x = Qpairi k n].
proof: Proof. split. move /funI_P => [z /setX_P [pe Pqz Qz] xe]. by exists (P z); exists (Q z). move=> [k [n [kB nB xe]]]; apply /funI_P; exists (J k n); aww. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)