proposition: Lemma aggregateE : aggregate b mul add = Ret \o foldl add b \o map (foldl mul b) :> (_ -> M _).
proof: Proof. rewrite -lemma31; last by move=> x ??; rewrite -addA (addC x) addA. by rewrite /aggregate 2!fcomp_def -compA. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib