proposition: Lemma CNFr_p3 f n i: natp n -> CNFr_ax f n -> i <c n -> oopow (f i) <=o CNFrv f n.
proof: Proof. move => nN ax lin;move: n nN ax i lin. apply:Nat_induction; first by move => _ u /clt0. move => n nN Hrec axr i /(cltSleP nN)/(cle_eqVlt);case => lin. by rewrite lin; apply:CNFr_p2. have ax0:=(CNFr_ax_s nN axr). apply: (oleT (Hrec ax0 i lin)). rewrite (CNFr_rec _ nN). exact:(osum_M0le (OS_CNFr_t axr (cltS nN)) (OS_CNFr0 nN ax0)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)