proposition: Lemma CNFr_p2 f n: natp n -> CNFr_ax f (csucc n) -> oopow (f n) <=o CNFrv f (csucc n).
proof: Proof. move => nN ax; move:(CNFr_ax_s nN ax) => axr. rewrite (CNFr_rec _ nN). exact: osum_Mle0 (OS_CNFr_t ax (cltS nN)) (OS_CNFr0 nN axr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)