proposition: Lemma nsv_cantor_p2 p: ordinalp p -> forall a b x y, a <o omega0 -> b <o omega0-> x <o oopow p -> y <o oopow p -> S (oopow p *o a +o x) (oopow p *o b +o y) = oopow p *o (a +o b) +o S x y.
proof: Proof. move: p; apply:least_ordinal2 => p op pp. have Ha x y: x <o oopow p -> y <o oopow p -> S x y <o oopow p. by apply: nsv_cantor_p1. have oop:=(OS_oopow op). have Hb a y: a <o omega0 -> y <o oopow p -> S (oopow p *o a) y = (oopow p) *o a +o y. move => lao; move: (proj31_1 lao) => oa;move: a oa lao y. apply:least_ordinal2 => b ob bp lbo y ys. move:(OS_prod2 oop ob) (proj31_1 ys) => of1 oy. move: y oy ys; apply:least_ordinal2 => y oy yp ys. apply: oleA; last exact: (nsv_ge_sum of1 oy). apply: (nsv_le_prop of1 oy (OS_sum2 of1 oy)); last first. move => x lxy; move:(olt_ltT lxy ys) => xs. rewrite (yp x lxy xs); apply: (osum_Meqlt lxy of1). move => x lxs. suff: S x y <o oopow p *o b. move => aux; apply: (olt_leT aux (osum_Mle0 of1 oy)). case:(ozero_dichot ob) => cbz. by move: lxs; rewrite cbz oprod0r => /olt0. have bN: natp b by apply/(oltP OS_omega). move: (cpred_pr bN (nesym (proj2 cbz))) => [pN pv]. have bv1: b = osucc (cpred b) by rewrite - succ_of_nat. have ox := proj31_1 lxs. move: (OS_nat pN) => opr. have cNN: cpred b <o omega0 by apply/(oltP OS_omega). have ps: cpred b <o b by rewrite {2}bv1; apply/oltS. have oopc:= (OS_prod2 oop opr). have eq1: oopow p *o b = oopow p *o (cpred b) +o (oopow p). by rewrite {1} bv1 (oprod2_succ oop opr). case: (oleT_el (OS_prod2 oop opr) ox) => cpx. move: (odiff_pr cpx) ; set d := _ -o _ ; move => [od dv]. move:(osum_Meqltr od oop oopc); rewrite - dv -eq1. move => h; move: (h lxs) => ds. move: (bp _ ps cNN _ ds); rewrite - dv => <-. move: (Ha _ _ ds ys)=> sdys. rewrite - (nsvA oopc od (proj31_1 ys)) (bp _ ps cNN _ sdys). by rewrite eq1; apply: osum_Meqlt. apply: (olt_ltT (nsv_ltl cpx (proj31_1 ys))); rewrite (bp _ ps cNN _ ys). by rewrite eq1; apply:osum_Meqlt. have Hc a b: a <o omega0 -> b <o omega0 -> S ((oopow p) *o a) ((oopow p) *o b) = oopow p *o (a +o b). move => alo; move:(proj31_1 alo) => oa. move: a oa alo b; apply:least_ordinal2 => a oa ap alo b blo. move:(proj31_1 blo) => ob; move: b ob blo. apply:least_ordinal2 => b ob bp blo. move:(OS_prod2 oop oa) (OS_prod2 oop ob) => of1 of2. apply: oleA; last by rewrite (oprodD oa ob oop); exact: (nsv_ge_sum of1 of2). apply: (nsv_le_prop of1 of2 (OS_prod2 oop (OS_sum2 oa ob))) => x xlt. have H u v: u <o omega0 -> v <o omega0 -> u +o v = v +o u. move => /(oltP OS_omega) uN /(oltP OS_omega) vN. by rewrite !osum2_2int // csumC. move: (odivision_exists oop oa xlt). set a1 := oquo _ _; set r := orem _ _. move => [[oa1 or xv rs] a1s]. have a1N := olt_ltT a1s alo. have of11 := OS_prod2 oop oa1. have a1bo: a1 +o b <o omega0 by apply: osum2_lt_omega. rewrite xv - (Hb _ _ a1N rs). rewrite (nsvC of11 or) - (nsvA or of11 of2) (ap _ a1s a1N _ blo). rewrite (nsvC or (OS_prod2 oop (OS_sum2 oa1 ob))) (Hb _ _ a1bo rs). apply: (olt_leT (osum_Meqlt rs (OS_prod2 oop (proj31_1 a1bo)))). rewrite - (oprod2_succ oop (proj31_1 a1bo)) (H _ _ a1N blo) (H _ _ alo blo). by apply: (oprod_Meqle _ oop); apply/oleSltP;apply/osum_Meqlt. move: (odivision_exists oop ob xlt). set b1 := oquo _ _; set r := orem _ _. move => [[ob1 or xv rs] b1s]. have b1N := olt_ltT b1s blo. have of11 := OS_prod2 oop ob1. have a1bo: a +o b1 <o omega0 by apply: osum2_lt_omega. rewrite xv - (Hb _ _ b1N rs). rewrite (nsvA of1 of11 or) (bp _ b1s b1N) (Hb _ _ a1bo rs). apply: (olt_leT (osum_Meqlt rs (OS_prod2 oop (OS_sum2 oa ob1)))). rewrite - (oprod2_succ oop (proj31_1 a1bo)). by apply: (oprod_Meqle _ oop); apply/oleSltP; apply/osum_Meqlt. move => a b x y aN bN xs ys. move: (proj31_1 aN) (proj31_1 bN) => oa ob. move: (proj31_1 xs) (proj31_1 ys) => ox oy. have abs: a +o b <o omega0 by apply: osum2_lt_omega. have xys:=(Ha _ _ xs ys). have ooab:= (OS_prod2 oop (OS_sum2 oa ob)). move:(OS_prod2 oop oa) (OS_prod2 oop ob) => of1 of2. hnf; rewrite - (Hb _ _ aN xs) - (Hb _ _ bN ys). by rewrite nsvACA // (Hc _ _ aN bN) Hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)