proposition: Lemma int_not_pair x: inc x Nat -> pairp x -> False.
proof: Proof. move => xN; rewrite /pairp kpairE /kpair_def => h. have ox :=(OS_nat xN). case: (equal_or_not emptyset x) => xne. rewrite - h in xne; empty_tac1 ((singleton (P x))). move /(oltP ox): (conj (ole0x ox) xne); rewrite - h /ord_zero. move => /set2_P; case => h3; empty_tac1 (P x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)