proposition: Lemma lemma45a (xss : seq (seq A)) : foldl mul b (flatten xss) = foldl add b (map (foldl mul b) xss).
proof: Proof. case: (@iperm_is_alt_ret M _ xss) => m Hm. have step1 : (Ret \o foldl mul b \o flatten) xss = (Ret \o foldl add b \o map (foldl mul b)) xss [~] fmap (foldl add b \o map (foldl mul b)) (m : M _). rewrite -H /aggregate iperm_o_map -fcomp_comp. by rewrite fcompE Hm alt_fmapDr fmapE /= bindretf. apply esym, idempotent_converse in step1. case: step1 => step11 step12. apply injective_return in step11. by rewrite -step11. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib