proposition: Lemma theorem46rid z zs : z = foldl mul b zs -> aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) -> z = add z b.
proof: Proof. move=> zzs H. transitivity (foldl mul b (flatten [:: zs; [::]])). by rewrite /= cats0. transitivity (foldl add b (map (foldl mul b) [:: zs; [::]])). have [m Hm] : exists m : M _, iperm [:: zs; [::]] = Ret [:: zs; [::]] [~] m. exact: iperm_is_alt_ret. by rewrite (lemma45a idempotent_converse injective_return H). rewrite /= -zzs. by rewrite -(@theorem46lid _ zs). Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib