proposition: Lemma ord_negl_p6 e f n: natp n -> CNFr_ax f (csucc n) -> e <o (f n) -> (oopow e) <<o (CNFrv f (csucc n)).
proof: Proof. move: OS_omega => oo nN h ef. have [[oe op _] _] :=ef. have o1:= OS_pow oo oe. have o2:= OS_pow oo op. have lt1:= (ord_negl_p4 ef). rewrite /CNFrv (osum_fS _ nN); apply: ord_negl_sum => //. exact:(OS_CNFr0 nN (CNFr_ax_s nN h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)