proposition: Lemma fsum_sub X Y : X `<=` Y -> fsum X <= fsum Y.
proof: Proof. move => sub. rewrite [fsum Y](fsumID (mem X)) [Z in _ <= fsum Z + _](_ : _ = X) ?leq_addr //=. apply: fset_ext => x. rewrite inE. move/subP : sub => /(_ x) ?. apply/andP/idP; tauto. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)