proposition: Lemma set_addS (F : nat -> D) k : set_add [set F i | i in [set x | 'I_k.+1 x]] = set_add [set F i | i in [set x | 'I_k x]] + F k.
proof: Proof. rewrite addrC -set_addDl; congr set_add; rewrite predeqP => x; split. - move=> -[i Hi] <-. move: (leq_ord i); rewrite leq_eqVlt => /orP[/eqP -> | {}Hi]; [by left|]. by right; exists (Ordinal Hi). - move=> [-> | [i _ <-]]; [by exists ord_max|]. by exists (inord i); rewrite ?inordK // ltnS ltnW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice