proposition: Lemma CNF_exp_bnd e c n e0: \2c <=o gamma -> ordinalp e0 -> natp n -> CNFb_ax e c n -> CNFbv e c n <o gamma ^o e0 -> (forall i, i <c n -> e i <o e0).
proof: Proof. move => le1 oe nN ax lt1 i id. case: (equal_or_not n \0c) => nz. by move: id; rewrite nz => /clt0. move: (cpred_pr nN nz) => [mN mv]. rewrite mv in ax id. move/(cltSleP mN): id => ipn. move:(CNF_exponents_M (NS_succ mN) (proj1 ax) ipn (cltS mN)) => ha. case (oleT_el oe (proj31 ha)) => // hb. move:(CNFq_pg4 mN ax); rewrite - mv => h1; move:(ole_ltT h1 lt1) => hc. by move: (opow_Meqle (olt_leT olt_02 le1) (oleT hb ha)) => /(oltNge hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)