fact: Definition commute {M : monad} A B (m : M A) (n : M B) C (f : A -> B -> M C) : Prop := m >>= (fun x => n >>= (fun y => f x y)) = n >>= (fun y => m >>= (fun x => f x y)) :> M _.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy