proposition: Lemma size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
proof: Proof. intros. rewrite (union_difference Y X) at 2 by done. rewrite size_union by set_solver. lia. Qed.
imports: stdpp(relations) stdpp(options)