proposition: Lemma CNFB_e_p5 e c n (x := CNFbv b e c (csucc n)): natp n -> CNFb_ax b e c (csucc n) -> (e n = x -> b_critical x) /\ (b_critical x -> (n = \0c /\ (e n = x))).
proof: Proof. move=> nN ax. move:(CNFq_p1 b e c nN); rewrite -/x. have bp :=(olt_leT olt_02 bg2). set en:= (e n);set A := cantor_mon _ _ _ _; set B := CNFbv _ _ _ _ => xv. have oen: ordinalp (e n). by move: (ax) => [[_ a2 _ _] _]; apply: (a2 _ (cltS nN)). have cnp := ((proj2 ax) _ (cltS nN)). move: (opow_Mspec2 oen bg2) => le1. have op:= proj32 le1. move: (oprod_Mle1 op cnp); rewrite -/(cantor_mon b e c n) -/A => le2. have oA:=(CNFq_p0 (proj1 ax) (cltS nN)). have le3: en <=o b *o en by apply oprod_M1le. have le4:= (oleT le3 le1). have le5:= (oleT le4 le2). have ax1:=(CNFb_p5 nN ax). have oB:= (OS_CNFq nN (proj1 ax1)). have le7:= (osum_Mle0 oA oB). have pg: en = x -> B = \0o. rewrite xv; move=> es; rewrite es in le5. exact (osum2_a_ab oA oB (oleA le5 le7)). split. by move=> ex; apply: oleA; [rewrite -{1} ex xv (pg ex) (osum0r oA) | ue]. rewrite /b_critical => ci. have le6: en <=o x. by rewrite xv; apply: (oleT le5); apply:osum_Mle0. move: (CNFq_pg1 nN (proj1 ax)); rewrite -/x -/e - {1} ci => le8. case: (equal_or_not en x) => nex; last first. have xx: osucc en <=o x by apply /oleSltP. case: (oltNge le8 (opow_Meqle bp xx)). split => //; ex_middle n0. move:(cpred_pr nN n0) => [mN mv]. move:(pg nex) ax1; rewrite /B mv => uu ax1. by move: (proj2 (CNFq_pg5 mN ax1)); rewrite uu. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)