proposition: Lemma CNFb_Al e c n (e1 := fun z => e (csucc z)) (c1 := fun z => c (csucc z)): natp n -> CNFb_axo e c (csucc n) -> [/\ ordinalp(cantor_mon omega0 e c \0o), CNFb_axo e1 c1 n & CNFbvo e c (csucc n) = CNFbvo e1 c1 n +o (cantor_mon omega0 e c \0o)].
proof: Proof. move => nN [ax1 ax2]; move:(CNFq_Al nN ax1) => [sa sb sc]; split => //. split => // i lin; apply: ax2; apply:(cltSS lin). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)