proposition: Lemma fmap_bind (A B C : UU0) (f : A -> B) m (g : C -> M A) : fmap f (m >>= g) = m >>= (f (o) g).
proof: Proof. rewrite fcomp_def fmapE bindA; bind_ext => c. by rewrite compE -/(fmap _ _) fmapE. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)