proposition: Lemma CNFr_p4' f n m: natp n -> CNFr_ax f (csucc n) -> f n <o m -> CNFrv f (csucc n) <o oopow m.
proof: Proof. move => nN ax /oleSltP lt1; apply: (olt_leT (CNFr_p4 nN ax)). by apply:opow_Mo_le. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)