proposition: Lemma refin_guard_le (M : plusMonad) (d : unit) (T : orderType d) (x y : T) : (guard (~~ (y <= x)%O) : M _) `<=` guard (x <= y)%O.
proof: Proof. rewrite -ltNge le_eqVlt. case: guardPn => H. rewrite orbT guardT; exact: refin_refl. by rewrite orbF /refin altfailm. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)