proposition: Lemma nds_same_deg_s_perm e (c r: fterm) n f (X := (fun i => oopow e *o (c i) +o r i)): natp n -> \0c <c n-> ordinalp e -> (forall i, i<c n -> \0o <o c i /\ r i <o oopow e) -> (forall i, i<c n -> c i <o omega0) -> inc f (permutations n) -> nds_sc X n f = oopow e *o (osumf c n) +o (r (Vf f \0c)).
proof: Proof. move => nN nz oe h1 h2 fp. move:(fp) => /Zo_P [] /functionsP [fz sz tz] bz. have sa: forall i, i <c n -> \0o <o c (Vf f i) /\ r (Vf f i) <o oopow e. move => i /(NltP nN) lin; apply: h1; apply /(NltP nN); Wtac. transitivity (osumf(fun i => oopow e *o (c (Vf f i)) +o r (Vf f i)) n). by apply:(osumf_exten nN) => i lin. have h3: forall i, i <c n -> natp (c i). by move => i /h2 /olt_omegaP. by rewrite (nds_same_deg_sn nN nz oe sa) - /(nds_sc c n f) (osum_of_nat_bis). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)