proposition: Lemma cnext_succ x: inc x E -> inc (osucc x) E.
proof: Proof. move=> cx; move/(cnextP (proj1 iC)):(cx) => [ox _]. rewrite - (osucc_pr ox); move: olt_1omega => [h _]. by apply: cnext_sum => //; apply:cnext_leomega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)