proposition: Lemma set_addU A B : set_add (A `|` B) = set_add A + set_add B.
proof: Proof. by rewrite set_joinU add_join. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice