proposition: Lemma fsum_replace X Y Z : fsum Z < fsum Y -> Y `<=` X -> fsum (Z `|` X `\` Y) < fsum X.
proof: Proof. move => ltn sub. rewrite fsumU (fsumDsub sub). apply: leq_ltn_trans (leq_subr _ _) _. rewrite -ltn_subRL. apply: ltn_sub2l => //. apply: leq_trans ltn _. exact: fsum_sub. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)