proposition: Lemma CNFB_e_p3 e c n: natp n -> CNFb_ax b e c (csucc n) -> e n <=o (CNFbv b e c (csucc n)).
proof: Proof. move => nB ax; move: (CNFq_pg4 nB ax) => sa. move:(ax) => [[_ sb _ _] _]; move: (sb _ (cltS nB)) => op. move: (oleT (opow_Mspec2 op bg2) sa) => le2. exact:(oleT (oprod_M1le (olt_leT olt_02 bg2) op) le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)