proposition: Lemma CNFq_pg2 e c n a: natp n -> CNFq_ax e c (csucc n) -> (e n) <o a -> CNFbv e c (csucc n) <o (gamma ^o a).
proof: Proof. move => pa pb pc; move: (CNFq_pg1 pa pb) => h. move/oleSltP: pc => pc. exact: (olt_leT h (opow_Meqle (CNFq_pg0 pb) pc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)