proposition: Lemma CNFq_pg1 e c n: natp n -> CNFq_ax e c (csucc n) -> CNFbv e c (csucc n) <o (gamma ^o (osucc (e n))).
proof: Proof. move: n;apply: Nat_induction. move => h; rewrite succ_zero (CNFq_p3 h (succ_positive \0c)). move: (h) => [bo ax1 ax2 _ ]. have szp:=(succ_positive \0c). move: (CNFq_pg0 h) (ax1 _ szp) (ax2 _ szp) => bp eo cb. rewrite /cantor_mon (opow_succ (proj32_1 bp) eo). exact:(oprod_Meqlt cb (opow_pos bp eo)). move=> n nN Hrec ax1. have sa:= (Hrec (CNFq_p5 (NS_succ nN) ax1)). move: (ax1) => [b2 _ ax3 ax2]. have snn:= (cltS (NS_succ nN)). move:(ax2 n nN snn) (CNFq_p0 ax1 snn) => /oleSltP lt1 o1. move:(olt_leT sa (opow_Meqle (CNFq_pg0 ax1) lt1)) => lt2. have ha:=proj32_1 lt2. have cm1:=(ax3 _ snn). have [[hb bb _] _]:= cm1. have oee := proj32 lt1. have lt3: gamma ^o e (csucc n) *o osucc (c (csucc n)) <=o gamma ^o osucc (e (csucc n)). by rewrite opow_succ //; apply: oprod_Meqle => //;move /oleSltP: cm1. move: (osum_Meqlt lt2 o1). rewrite (CNFq_p1 _ _ (NS_succ nN)) {2}/cantor_mon - (oprod2_succ ha hb) => h1. exact: (olt_leT h1 lt3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)