proposition: Lemma set_add_lim_nat (F : nat -> D) l : (forall k, set_add [set F i | i in [set x | 'I_k x]] <= l) -> set_add (range F) <= l.
proof: Proof. move=> H; apply: set_join_le_ub => _ [i _ <-]. by move: (H i.+1); apply/le_trans/set_join_ub; exists ord_max. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice