proposition: Lemma fset_map_compose `{FSet A} `{FSet B} `{FSet C} (f : B → C) `{!Setoid_Morphism f} (g : A → B) `{!Setoid_Morphism g} : fset_map (f ∘ g) = fset_map f ∘ fset_map g.
proof: Proof. pose proof (fset_car_setoid A). symmetry. apply (fset_map_unique (f ∘ g) _). rewrite compose_assoc. rewrite <-(fset_map_correct g). rewrite <-compose_assoc. rewrite (fset_map_correct f). now apply setoids.ext_equiv_refl. 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