proposition: Lemma nds_same_deg_sn e (c r: fterm) n: natp n -> \0c <c n -> ordinalp e -> (forall i, i<c n -> \0o <o c i /\ r i <o oopow e) -> osumf (fun i => oopow e *o (c i) +o r i) n = oopow e *o (osumf c n) +o (r \0c).
proof: Proof. move => nN nz oe. have op := (OS_oopow oe). move: (cpred_pr nN (nesym (proj2 nz))) => [pN ->]. move: (cpred n) pN; clear n nN nz; apply: Nat_induction. rewrite succ_zero => H. move: (H _ (clt_01)) => [[[_ oc _] _] [[or _ _] _]]. have ot:= (OS_sum2 (OS_prod2 op oc) or). by rewrite (osum_f1 oc) (osum_f1). move => n nN Hrec ol. move:(true_below_rec (NS_succ nN) ol) => [sa [/proj32_1 ocn rs]]. move:(proj31_1 (proj2(sa _ (succ_positive n)))) => or0. rewrite (osum_fS _ (NS_succ nN)) (Hrec sa). move:(true_below_rec nN sa) => [sb [[/proj32 oc0 /nesym cnz]_]]. have pc: \0o <o osumf c (csucc n). have /(OS_osumf nN) ha: nds_ax c n by move => i /sb [/proj32_1 ]. rewrite (osum_fS _ nN); apply: (ord_ne0_pos (OS_sum2 oc0 ha)). by case/(osum2_zero oc0 ha). by rewrite (nds_same_deg_s2 oe ocn rs pc or0) (osum_fS _ (NS_succ nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)