proposition: Lemma CNF_simple_bnd a n b x: CNF_simple_ax a n b x -> inc (J a (J n b)) (osucc x \times (Nat \times x)).
proof: Proof. move => hx; move:(CNF_simple_p1 hx) => [ha hb hc [hd he hf hg]]. move:(proj1 (ord_eps_p2 ha hg hc)); rewrite - hd => ax. move:(CNF_simple_p2 hx) => [_ bx1 _]. have bx: inc b x by apply/(oltP (proj32 ax)). move/ (oleP (proj32 ax)): ax => asx. move: hx => [_ _ nN _ _]. apply: (setXp_i asx); apply:(setXp_i nN bx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)