proposition: Lemma commutativity_of_assertions A q : Join \o (M # (bassert q)) = bassert q \o Join :> (_ -> M A).
proof: Proof. by apply boolp.funext => x; rewrite !compE join_fmap /bassert joinE bindA. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra Rstruct reals) infotheo(Reals_ext) infotheo(realType_ext) monae_lib HB(structures)