proposition: Lemma set_addDl a B : set_add (a |` B) = a + set_add B.
proof: Proof. apply/le_anti/andP; split. - apply: set_join_le_ub => x [-> | Bx]; [exact: led_addr|]. by apply: le_trans (led_addl _ _); apply: set_join_ub. - by rewrite led_addE set_joinU_ge_r andbT -[leLHS](set_join1 a) set_joinU_ge_l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice