proposition: Lemma set_add_led (F : nat -> D) k : set_add [set F i | i in [set x | 'I_k x]] <= set_add (range F).
proof: Proof. elim: k => [|k IHk]. - set S := image _ _. have ->: S = set0 by rewrite -subset0 => x [[]]. by rewrite set_join0 le0x. - rewrite set_addS led_addE IHk /=. by apply: set_join_ub; exists k. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice