proposition: Lemma cnfnat_sum_mon n a b: ordinalp n -> a <o omega0 -> b <o omega0-> (oopow n *o a +#o oopow n *o b) = (oopow n *o (a +o b)).
proof: Proof. move => on lao lbo. move: (proj31_1 lao) (proj31_1 lbo) => oa ob. have ooa:= (OS_prod2 (OS_oopow on) oa). have oob:= (OS_prod2 (OS_oopow on) ob). case: (ozero_dichot oa) => az. by rewrite az (osum0l ob) oprod0r natural_sumC (natural_sum0 oob). case: (ozero_dichot ob) => bz. by rewrite bz (osum0r oa) oprod0r (natural_sum0 ooa). have pa: posnatp a by apply/ posnat_ordinalp. have pb: posnatp b by apply/ posnat_ordinalp. move: (cnf_one_term on pa); set A := Lg _ _; move => [cA _ eqA1 eqA2]. move: (cnf_one_term on pb); set B := Lg _ _; move => [cB _ eqB1 eqB2]. have eab: a +o b = a +c b by rewrite osum2_2int //; apply/olt_omegaP. have pc: posnatp (a +o b) by rewrite eab; apply: (posnat_csum2 pa pb). move: (cnf_one_term on pc); set C := Lg _ _; move => [cC _ eqC1 eqC2]. rewrite /natural_sum eqA1 eqB1 - eqC2; congr cnf_val. symmetry; apply: (cnf_nat_sum_p3 cA cB cC) => e. rewrite ! Vr_monomial. by case: (equal_or_not e n) => en; Ytac0; Ytac0; Ytac0 => //; rewrite (csum0r CS0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)