fact: Definition mpair {M : monad} {A} (xy : (M A * M A)%type) : M (A * A)%type := let (mx, my) := xy in mx >>= (fun x => my >>= fun y => Ret (x, y)).
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy