proposition: Lemma set_add1 (F : nat -> D) : set_add [set F i | i in [set x | 'I_1 x]] = F O.
proof: Proof. rewrite -(addr0 (F O)) -bottom_zero -set_join0 -set_addDl setU0; congr set_add. by rewrite predeqP => x; split=> [[y] | ->]; [rewrite ord1|exists ord0]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice