proposition: Lemma refin_bind (M : plusMonad) A B {m n : M A} {f g : A -> M B} : m `<=` n -> f `<.=` g -> (m >>= f) `<=` (n >>= g).
proof: Proof. by move=> mn /refin_bindl ?; exact: (refin_trans _ (refin_bindr _ mn)). Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)