proposition: Lemma fmap_comp {A B C} (f : B -> C) (g : A -> B) F: Filter F -> (f \o g)%FUN @ F = f @ (g @ F).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed