proposition: Lemma nsv_cantor_p2_ww p: ordinalp p -> forall a b x y, a <o omega0 -> b <o omega0-> x <o oopow p -> y <o oopow p -> (oopow p *o a +o x) +#o (oopow p *o b +o y) = oopow p *o (a +o b) +o (x +#o y).
proof: Proof. move => op a b x y ha hb hx hy. rewrite (cnfnat_sum_rem op ha hx) (cnfnat_sum_rem op hb hy). have ox := (proj31_1 hx). have oy := (proj31_1 hy). have oa := (proj31_1 ha). have ob := (proj31_1 hb). move: (OS_prod2 (OS_oopow op) oa) (OS_prod2 (OS_oopow op) ob) => ooa oob. have abs: a +o b <o omega0 by apply: osum2_lt_omega. have eab : (b +o a) = (a +o b). move/olt_omegaP: ha => aN; move/olt_omegaP: hb => bN. by rewrite osum2_2int // osum2_2int // csumC. have ow: ordinalp (oopow p *o a +#o x) by apply: OS_natural_sum. rewrite (natural_sumC _ y)(natural_sumA ow oy oob). rewrite - [in X in (X +#o _ = _)] (natural_sumA ooa ox oy) natural_sumC. rewrite (natural_sumA oob ooa (OS_natural_sum ox oy)). move: (natural_small op hx hy) => ss. rewrite (cnfnat_sum_mon op hb ha) eab. by rewrite (cnfnat_sum_rem op abs ss). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)