proposition: Lemma refin_bindr (M : altMonad) A B (m1 m2 : M A) (f : A -> M B) : (m1 `<=` m2) -> (m1 >>= f `<=` m2 >>= f).
proof: Proof. by move=> m12; rewrite /refin -alt_bindDl m12. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)