proposition: Lemma CNFr_p4 f n: natp n -> CNFr_ax f (csucc n) -> CNFrv f (csucc n) <o oopow (osucc (f n)).
proof: Proof. have Hi i: ordinalp i -> oopow i <o oopow (osucc i). move => oi; apply:(opow_Mo_lt (oltS oi)). move:n; apply:Nat_induction. move=> ax; move: (proj1 ax \0c (cltS NS0)) => of0. rewrite succ_zero /CNFrv (osum_f1 (f:= oopow \o f) (OS_oopow of0)). by apply:Hi. move => n nN Hrec ax. move:(proj2 ax n nN (cltS (NS_succ nN))) => le1; move: (proj32 le1) => of0. move/(oleSSP): le1 => /opow_Mo_le le2. move:(olt_leT (Hrec (CNFr_ax_s (NS_succ nN) ax)) le2)=> ww. rewrite (CNFr_rec _ (NS_succ nN)). apply: (indecomp_prop2 (Hi _ of0) ww (indecomp_prop4 (OS_succ of0))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)