proposition: Lemma eq_bind (M : monad) (A B : UU0) (m : M A) (f1 f2 : A -> M B) : f1 =1 f2 -> m >>= f1 = m >>= f2.
proof: Proof. by move=> f12; congr bind; apply boolp.funext. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra Rstruct reals) infotheo(Reals_ext) infotheo(realType_ext) monae_lib HB(structures)