proposition: Lemma CNF_simple_p2 a n b x: CNF_simple_ax a n b x -> [/\ a <=o x, b <o x & oopow a <=o 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: hx => [_ _ nN _ _]. have oa:=(proj32_1 he). have on:=(OS_nat nN). have ob:=(OS_prod2 oa on). have pa: omega0 ^o a *o csucc n = omega0 ^o a +o omega0 ^o a *o n. rewrite (Nsucc_rw nN) csumC - (osum2_2int NS1 nN) (oprodD OS1 on oa). rewrite oprod1r //. have hi: omega0 ^o a <=o x. rewrite hd pa -(osumA oa ob hc); apply: (osum_Mle0 oa (OS_sum2 ob hc)). split => //;exact:olt_leT he hi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)