proposition: Lemma guardsC (HM : BindLaws.right_zero (@bind M) (@fail _)) b B (m : M B) : guard b >> m = m >>= assert (fun=> b).
proof: Proof. case: guardPn => Hb. - rewrite bindskipf. under eq_bind do rewrite assertT. by rewrite bindmret. - under [RHS]eq_bind do rewrite assertF. by rewrite bindfailf HM. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)