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