proposition: Lemma CNFb_exists a: ordinalp a -> \2c <=o gamma -> exists e c n, [/\ CNFb_ax e c n, natp n & a = CNFbv e c n].
proof: Proof. move=> oa oeb. pose p a := exists e c n, [/\ CNFb_ax e c n, natp n & a = CNFbv e c n]. apply: (least_ordinal2 (p := p)) oa => y oy p2. case: (equal_or_not y \0o) => ynz. exists (@id Set), (@id Set), \0c; split; first split. + split => // i; try move /clt0 => //. by move => _ /clt0. + by move => i /clt0. + fprops. + by rewrite CNFq_p2. move: OS2 => o2. have cpy1:=(ord_ne0_pos oy ynz). move: (ord_ext_div_exists oeb cpy1) => [e1 [c1 [rm [oe1 oc1 or [eq1 lt1 lt2 lt3]]]]]. have rmy: rm <o y. have p5:=(OS_pow (proj32_1 lt2) oe1). have p3: (gamma ^o e1) <=o ((gamma ^o e1) *o c1) by apply: oprod_Mle1. move: (osum_Mle0 (proj32 p3) or); rewrite - eq1 => p4. exact : (olt_leT lt1 (oleT p3 p4)). move: (p2 _ rmy) => [e [c [n [ax nN rv]]]]. have snN:= (NS_succ nN). pose e' i := Yo (i = n) e1 (e i). pose c' i := Yo (i = n) c1 (c i). exists e', c', (csucc n). have ha: CNFbv e' c' n = CNFbv e c n. rewrite /CNFbv; apply: osumf_exten => // i [ _ lin]. by rewrite /e' /c' /cantor_mon; Ytac0; Ytac0. have hb: cantor_mon e' c' n = gamma ^o e1 *o c1. by rewrite /cantor_mon /e' /c'; Ytac0; Ytac0. rewrite (CNFq_p1 _ _ nN) ha - rv hb - eq1. suff: CNFb_ax e' c' (csucc n) by move => hc; split. move: (CNF_exp_bnd oeb oe1 nN ax); rewrite - rv => hx. move: ax => [[a1 a2 a3 a4] a5]; split; last first. rewrite /c';move => i /(cltSleP nN); case (equal_or_not i n). by move => -> _; Ytac0. move => i1 i2; Ytac0; exact: (a5 _ (conj i2 i1)). split; first done. + rewrite /e';move => i /(cltSleP nN); case (equal_or_not i n). by move => -> _; Ytac0. move => i1 i2; Ytac0; exact: (a2 _ (conj i2 i1)). + rewrite /c';move => i /(cltSleP nN); case (equal_or_not i n). by move => -> _; Ytac0. move => i1 i2; Ytac0; exact: (a3 _ (conj i2 i1)). + rewrite /e';move => i iN /(cltSleP nN) sin. have isi:= (clt_leT (cltS iN) sin). move: (proj2 isi) => nin; Ytac0. case (equal_or_not (csucc i) n) => ne1; Ytac0; first by exact: (hx lt1 _ isi). exact:(a4 i iN (conj sin ne1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)