proposition: Lemma workE : let next := fun n (mx : M _) => if n == 0 then fail else fmap (muln n) mx in work = foldr next (Ret 1).
proof: Proof. apply foldr_universal => // h t; case: ifPn => [/eqP -> //| h0]. by rewrite /work inE eq_sym (negbTE h0) [_ || _]/= fmap_if fmap_fail. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)