proposition: Lemma crunnewchk A T (m : M A) s : crun m -> crun (m >>= fun x => cnew T (s x) >>= cchk).
proof: Proof. under eq_bind do rewrite /cchk cnewget. rewrite -bindA crunmskip. exact: crunnew. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy