proposition: Lemma cnewgetret T s : cnew T s >>= @cget _ _ _ _ _ = cnew T s >> Ret s :> M _.
proof: Proof. under eq_bind do rewrite -cgetret; by rewrite cnewget. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy