proposition: Lemma CNFp_p2 e c n (a:= e n -o (e (cpred n))) (b := c n): CNFb_axo e c (csucc n) -> natp n -> n <> \0c -> [/\ \0o <o a, posnatp b & CNFbvo e c (csucc n) = (CNFbvo e c n) *o (CNFp_value1 a b)].
proof: Proof. move => ax nN nz. move: (cpred_pr nN nz) => [pnN pn]. move: (ax) => [[_ _ pe pf] pg]. have nn:= (cltS nN). have lt1: e (cpred n) <o e n. move: nn; rewrite {1 4} pn => h; exact:(pf _ pnN h). move: (odiff_pos lt1);move: lt1 => [le1 _]; move: (odiff_pr le1) => [oa pi] pj. move:(pg _ nn) (pe _ nn) => pa pb. rewrite -/a in oa. have pnb: posnatp b by apply/posnat_ordinalp. split => //. have ax2:= (CNFb_p5 nN ax). have od1 := OS_pow OS_omega oa. have ocn := (proj32_1 pa). have oc1 := (proj31 le1). have pc:= (OS_CNFb nN ax2); rewrite pn in ax2. move: (ord_rev_pred pj) =>[]; rewrite -/a => osa av. have od2 := OS_pow OS_omega osa. rewrite /CNFbvo (CNFq_p1 _ _ _ nN) /CNFp_value1. rewrite (oprod2_succ pc (OS_prod2 od1 ocn)); apply: f_equal2; last exact. rewrite (oprodA pc od1 ocn)/cantor_mon; apply: f_equal2; last exact. rewrite pi (opow_sum OS_omega oc1 oa) av (opow_sum OS_omega OS1 osa). rewrite (opowx1 OS_omega)(oprodA (OS_pow OS_omega oc1) OS_omega od2). rewrite (oprodA pc OS_omega od2); apply: f_equal2; last exact. move: (the_cnf_p5 pnN ax2); rewrite - pn;set v := CNFbvo _ _ _; move => [vp dv]. by rewrite - dv (CNF_prod_pr2bis vp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)