proposition: Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
proof: Proof. rewrite <-size_union by set_solver. setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by set_solver. rewrite <-union_difference, (comm (∪)); set_solver. Qed.
imports: stdpp(relations) stdpp(options)