proposition: Lemma fct_sum_rev f n (I := (csucc n)): natp n -> csumb I f = csumb I (fun i=> f (n -c i)).
proof: Proof. move=> nN. have snN:= NS_succ nN. apply: csum_Cn2; split. + by move=> x /(NleP nN) [_ cn _];apply /(NleP nN); apply: cdiff_ab_le_a. + move=> x y /(NleP nN) xn /(NleP nN) yn => h. by rewrite - (double_diff nN xn) -(double_diff nN yn) h. + aw => y /(NleP nN) yn; rewrite -(double_diff nN yn). exists (n -c y) => //; apply /(NleP nN). exact: (cdiff_ab_le_a _ (proj32 yn)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)