proposition: Lemma nds_same_deg_s2 e c1 c2 r1 r2: ordinalp e -> ordinalp c1 -> r1 <o oopow e -> \0o <o c2 -> ordinalp r2 -> (oopow e *o c1 +o r1) +o (oopow e *o c2 +o r2) = (oopow e *o (c1 +o c2) +o r2).
proof: Proof. set p := oopow e;move => oe oc1 pa pb or2. have op := OS_oopow oe. have or1:= (proj31_1 pa). have oc2:= (proj32_1 pb). have oa := OS_prod2 op oc1. have ob := OS_prod2 op oc2. have oc := OS_sum2 ob or2. have H:=(ord_negl_prod or1 op pb (indecomp_prop1 (indecomp_prop4 oe) pa)). rewrite - (osumA oa or1 oc) (osumA or1 ob or2) H (osumA oa ob or2). by rewrite - (oprodD oc1 oc2 op). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)