proposition: Lemma osum_of_nat_bis n X f: natp n -> (forall i, i <c n -> natp (X i)) -> inc f (permutations n) -> nds_sc X n f = osumf X n.
proof: Proof. move => nN ax /permutationsP[bf sf tf]. have ax2: forall i, i <c n -> natp (X (Vf f i)). move => i /(NltP nN) libe; apply: ax;apply/(NltP nN). move: (proj1 (proj1 bf)) => ff; Wtac. rewrite /nds_sc ! osum_of_nat // -{1} sf - tf. have qb: quasi_bij (Vf f) (source f) (target f). move:bf => [[ff hh] [_ sj]]; split => // t tsf; Wtac. by rewrite (csum_Cn2 X qb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)