proposition: Lemma CNFq_pg5 e c n: natp n -> CNFb_ax e c (csucc n) -> \0o <o CNFbv e c (csucc n).
proof: Proof. move => nN ax. move: (opow_pos (CNFq_pg0 (proj1 ax)) (CNFb_p8 ax nN)) => cp. exact:(olt_leT cp (CNFq_pg4 nN ax)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)