proposition: Lemma CNFq_pg4 e c n: natp n -> CNFb_ax e c (csucc n) -> (gamma ^o (e n)) <=o CNFbv e c (csucc n).
proof: Proof. move => nN [ax ax2]; move: (ax) => [b2 ax3 _ _]. have nn:= (cltS nN). have pa:= (oprod_Mle1 (OS_pow (proj32 b2) (ax3 _ nn)) (ax2 _ nn)). rewrite (CNFq_p1 _ _ nN). exact: (oleT pa (osum_Mle0 (proj32 pa) (OS_CNFq nN (CNFq_p5 nN ax)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)