fact: Definition bind_right_distributive (add : forall B, M B -> M B -> M B) := forall A B (m : M A) (k1 k2 : A -> M B), m >>= (fun x => add _ (k1 x) (k2 x)) = add _ (m >>= k1) (m >>= k2).
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)