proposition: Lemma fct_sum_const1 f n m: natp n -> (forall i, i <c n -> f i = m) -> csumb n f = n *c m.
proof: Proof. move=> nN p. by rewrite cprodC - csum_of_same; apply: csumb_exten => i /(NltP nN) /p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)