proposition: Lemma CNFq_Al e c n (e1 := fun z => e (csucc z)) (c1 := fun z => c (csucc z)): natp n -> CNFq_ax e c (csucc n) -> [/\ ordinalp(cantor_mon e c \0c), CNFq_ax e1 c1 n & CNFbv e c (csucc n) = CNFbv e1 c1 n +o (cantor_mon e c \0c)].
proof: Proof. move => nN ax. have h1: forall i, i<c n -> (cnf_s e \1c) i = e1 i. move => i lin; rewrite /cnf_s /e1 csucc_pr4 //; exact (proj31_1 lin). have h2: forall i, i<c n -> (cnf_s c \1c) i = c1 i. move => i lin; rewrite /cnf_s /c1 csucc_pr4 //; exact (proj31_1 lin). have eq1: csucc n = \1c +c n by rewrite csumC; exact:(Nsucc_rw nN). rewrite eq1 in ax; move: (CNFq_A NS1 nN ax) => [sa sb sc]. have lt1: \0c <c (\1c +c n) by rewrite - eq1; apply: succ_positive. rewrite eq1 sc (CNFq_p3 ax lt1). move:(CNFq_exten h1 h2 sb nN) => [ax1 ->]; split => //. by apply:(CNFq_p0 ax lt1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)