proposition: Lemma CNFb_change_nv e c n m (c':= (cnf_c c n (m +o (c n)))): natp n -> CNFb_axo e c (csucc n) -> m <o omega0 -> (CNFb_axo e c' (csucc n) /\ CNFbvo e c' (csucc n) = omega0 ^o (e n) *o m +o CNFbvo e c (csucc n)).
proof: Proof. move => nN ax mo. have nn:= cltS nN. have om:=proj31_1 mo. move: (ax) => [ [_ a0 a1 _] a2]. move: (a2 _ nn) => [[_ ocn _] nnz]. have pa:= (osum2_lt_omega mo (a1 _ nn)). have pb: \0o <o m +o c n. apply: (ord_ne0_pos (proj31_1 pa)). by move => h; move:(osum2_zero om ocn h) => [_ ]; apply: nesym. move: (CNF_c_ax n pb pa ax); rewrite -/c' => ax2; split; first by exact. have pc:= (OS_pow OS_omega (a0 _ nn)). have pd:= CNFq_p0 (proj1 ax) nn. have pe:=(OS_CNFq nN (CNFq_p5 nN (proj1 ax))). rewrite /CNFbvo. rewrite ! (CNFq_p1 _ _ _ nN) (osumA (OS_prod2 pc om) pd pe); apply: f_equal2. rewrite /cantor_mon /c' /cnf_c; Ytac0. by rewrite (oprodD om ocn pc). apply: (osumf_exten nN) => i [_ lin]. by rewrite /cantor_mon /c' /cnf_c; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)