proposition: Lemma CNF_simple_bdn2 x (z := the_CNF_simpl x): \0o <o x -> x <o epsilon0 -> ( P z <o x /\ (Q (Q z)) <o x).
proof: Proof. move => h hx. move: (the_CNF_simplP h). set a :=(P (the_CNF_simpl x)). set b:= (P (Q (the_CNF_simpl x))). set c:= (Q (Q (the_CNF_simpl x))). move => h1. move:(CNF_simple_bnd h1) => /setX_P [_ _ /setX_P[_ _]]; aw. move/(oltP (proj32_1 h)) => cx; split => //. move/CNF_simple_p1: h1 =>[ha hb hc [hd he hf hg]]. by move:(ord_eps_p2_bis ha hg hc);rewrite - hd; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)