proposition: Lemma nsv_cantor_p1 p: ordinalp p -> (forall q, q <o p -> (forall a b x y, a <o omega0 -> b <o omega0 -> x <o oopow q -> y <o oopow q -> S (oopow q *o a +o x) (oopow q *o b +o y) = oopow q *o (a +o b) +o S x y)) -> forall x y, x <o oopow p -> y <o oopow p -> S x y <o oopow p.
proof: Proof. move => op Hp. move: (oleR op); move: op. move: {-3}(p); apply:least_ordinal2 => t ot tp lt1p x y xlt ylt. move: (proj31_1 xlt) (proj31_1 ylt) => ox oy. case: (ozero_dichot ox); first by move => ->; rewrite nsv_0n. case: (ozero_dichot oy); first by move => ->; rewrite nsv_n0. move => yp xp. move: (the_cnf_p6 ot xp xlt)(the_cnf_p6 ot yp ylt) => dx dy. case: (omax_p1 (proj31_1 dx) (proj31_1 dy)). set d := omax (odegree x) (odegree y) => lext leyt. have lt: d <o t by rewrite /d/omax/Gmax; Ytac h. move: (nsv_aux xp lext) => [c1 [r1 [lc1 r1s xv]]]. move: (nsv_aux yp leyt) => [c2 [r2 [lc2 r2s yv]]]. move:(Hp _ (olt_leT lt lt1p) _ _ _ _ lc1 lc2 r1s r2s). rewrite xv yv; move ->. have hu:= (opow_Mo_lt lt). move: (olt_ltT (tp _ lt (oleT (proj1 lt) lt1p) _ _ r1s r2s) hu) => lt2. apply: indecomp_prop2 lt2 (indecomp_prop4 ot). move/(oltP OS_omega): lc1 => c1N. move/(oltP OS_omega): lc2 => c2N. rewrite (osum2_2int c1N c2N). move:(NS_sum c1N c2N); move:(c1 +c c2); apply: Nat_induction. by rewrite oprod0r; apply: oopow_pos. move => n nN H; rewrite (succ_of_nat nN). rewrite (oprod2_succ (OS_oopow (proj31_1 lt)) (OS_nat nN)). apply: (indecomp_prop2 H hu (indecomp_prop4 ot)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)