Rename multiset "union" into "disjoint union"

This fixes #13 (closed). Now ∪ and ∩ are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas ⊎ is the "sum" (i.e. adding the multiplicities).

Some questions/remarks:

• ⊎ and ∪ have different heights in my font (see ⊎∪). Is there maybe a better disjoint union symbol in unicode?
• There are probably all kinds of laws about the interaction between ∪, ∩, and ⊎, like distributivity. I did not attempt to prove a comprehensive set of such laws.
• ∖ is still the operation that subtracts multiplicity. I think that's fine, since there is no sensible difference operator for multisets that matches up with the union operator.

theories/base.v

@@ -782,6 +782,14 @@ Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪)
 Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
+Class DisjUnion A := disj_union: A → A → A.
+Hint Mode DisjUnion ! : typeclass_instances.
+Instance: Params (@disj_union) 2 := {}.
+Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
+Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
+Notation "( x ⊎)" := (disj_union x) (only parsing) : stdpp_scope.
+Notation "(⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
+
 Class Intersection A := intersection: A → A → A.
 Hint Mode Intersection ! : typeclass_instances.
 Instance: Params (@intersection) 2 := {}.