proposition: Lemma preserves_notin `{FullFSet A} `{FullFSet B} (f : A → B) `{!Inverse f} `{!Bijective f} x X : f x ∉ fset_map f X ↔ x ∉ X.
proof: Proof. split; intros E ?; now apply E, (preserves_in f). 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