proposition: Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X.
proof: Proof. intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition]. destruct (decide (x ∈ X)); intuition. Qed.
imports: stdpp(finite) stdpp(options)