proposition: Lemma cnext_leomega x: x <=o omega0 -> inc x E.
proof: Proof. move: iC => [cc _]. move => [ox oo xo]; apply /(cnextP cc); split => //. have: cardinal x <=c cardinal Nat by apply: sub_smaller. rewrite cardinal_Nat;move /infinite_c_P2: iC => h1 h2; apply: cleT h2 h1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)