proposition: Lemma add_join a b : a + b = a `|` b.
proof: Proof. by rewrite -[in LHS](set_join1 b) -set_addDl set_joinU !set_join1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice