proposition: Lemma fsizeU (T : choiceType) (X Y : {fset T}) : size (X `|` Y) <= size X + size Y.
proof: Proof. by rewrite -[size (_ `|` _)]fsum_const1 fsumU !fsum_const1 leq_subr. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)