proposition: Lemma CNFq_pg3 e c n a: natp n -> CNFq_ax e c n -> ordinalp a -> (forall i, i <c n -> e i <o a) -> CNFbv e c n <o (gamma ^o a).
proof: Proof. move => nN ax oa h; move: (CNFq_pg0 ax) => bp. case: (equal_or_not n \0c) => nz. rewrite nz CNFq_p2 //; apply: opow_pos; fprops. move: (cpred_pr nN nz) => [qa qb]. rewrite qb in h ax. have sa: (e (cpred n)) <o a by apply: h; apply: (cltS qa). rewrite qb; exact:(CNFq_pg2 qa ax). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)