proposition: Lemma CNFq_pg e c n: natp n -> CNFq_ax e c (csucc n) -> CNFbv e c n <o (gamma ^o (e n)).
proof: Proof. move => nN ax. move: (ax) => [_ ax2 _ _]. exact:(CNFq_pg3 nN (CNFq_p5 nN ax) (ax2 _ (cltS nN)) (CNFq_p6 nN ax)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)