proposition: Lemma fsum_const X n : {in X, const n w} -> fsum X = n * size X.
proof: Proof. move => C. rewrite [fsum X](_ : _ = \sum_(x <- X) n). - by rewrite big_const_seq count_predT iter_addn_0. - rewrite /fsum !big_seq. exact: congr_big. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)