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