proposition: Lemma ord_negl_p8 ep cp p en cn n: CNFb_axo ep cp (csucc p) -> CNFb_axo en cn (csucc n) -> natp p -> natp n -> ep p <o en n -> (CNFbvo ep cp (csucc p)) <<o (CNFbvo en cn (csucc n)).
proof: Proof. move => axp axn pN nN ln. have snN:= NS_succ nN. set x := CNFbvo en cn (csucc n). have aux: forall e c, c <o omega0 -> e <o (en n) -> ((omega0 ^o e) *o c) <<o x. move => e c cb ef; rewrite /x. move: (proj31_1 ef) (proj31_1 cb) => oe oc. have om:=(CNFq_p0 (proj1 axn) (cltS nN)). rewrite /CNFbvo (CNFq_p1 _ _ _ nN). apply: (ord_negl_sum (OS_prod2 (OS_pow OS_omega oe) oc) om). exact: (OS_CNFq nN (CNFq_p5 nN (proj1 axn))). apply: (ord_negl_p5 cb ef) (proj2 axn _ (cltS nN)). move:p pN axp ln; apply: Nat_induction. move => ax1 lt1; move:(ax1) => [[_ _ hc _] _]. rewrite /CNFbvo succ_zero (CNFq_p3 (proj1 ax1) (succ_positive \0c)). exact: (aux _ _ (hc _ (succ_positive \0c)) lt1). move => p pN Hrec ax1 l1. have spN:= (NS_succ pN). have axr:=(CNFb_p5 spN ax1). have spp:= (cltS spN). move:(proj1 ax1) => [_ _ hc ha]. have h0:= (olt_leT (ha p pN spp) (proj1 l1)). have h1 :=(CNFq_p0 (proj1 ax1) spp). have h6: cp (csucc p) <o omega0 by apply: (hc _ spp). have ox: ordinalp x by apply:OS_CNFb. rewrite /CNFbvo (CNFq_p1 _ _ _ spN). apply/(ord_negl_sum1 h1 (OS_CNFb spN axr) ox). split; [ exact: (aux _ _ h6 l1) | exact: (Hrec axr h0)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)