proposition: Lemma set_add0 (F : nat -> D) : set_add [set F i | i in [set x | 'I_0 x]] = 0%R.
proof: Proof. by rewrite -bottom_zero -set_join0; congr set_add; rewrite -subset0 => x [[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice