proposition: Lemma fsum_const1 (T : choiceType) (X : {fset T}) : fsum (fun _ => 1) X = size X.
proof: Proof. rewrite -[size X]mul1n. exact: fsum_const. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)