fact: Definition guard_or {E} (e : E) `{MThrow E M, MRet M} P `{Decision P} : M P := match decide P with | left H => mret H | right _ => mthrow e end.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)