proposition: Lemma list_extend_add x l : fset_extend f ({{x}} ⊔ l) = f x ⊔ fset_extend f l.
proof: Proof. destruct l as [l Pl]. unfold fset_extend, list_extend. simpl. clear Pl. induction l; simpl; [easy|]. case (decide_rel _); intros E. now rewrite E, associativity, (idempotency (&) _). now rewrite IHl, 2!associativity, (commutativity (f _)). Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders MathClasses.theory.lattices MathClasses.orders.lattices