proposition: Lemma diff_meet_join_diff X Y Z : X ∖ (Y ⊓ Z) = X ∖ Y ⊔ X ∖ Z.
proof: Proof. apply fset_eq_in. intro. repeat (rewrite fset_in_join || rewrite fset_in_meet || rewrite fset_in_difference). split; try tauto. intros [??]. case (decide (x ∈ Y)); tauto. Qed.
imports: MathClasses.theory.lattices MathClasses.varieties.monoids MathClasses.implementations.bool MathClasses.implementations.list_finite_set MathClasses.orders.lattices MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders