proposition: Lemma theorem46C x xs y ys : x = foldl mul b xs -> y = foldl mul b ys -> aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) -> add x y = add y x.
proof: Proof. move=> xxs yys. transitivity (add x (add y b)). by rewrite -(theorem46rid idempotent_converse injective_return yys). transitivity (foldl add b (map (foldl mul b) [:: xs; ys])). rewrite /= -xxs -yys. rewrite -(theorem46rid idempotent_converse injective_return yys) //. by rewrite -(theorem46lid idempotent_converse injective_return xxs). transitivity (foldl add b (map (foldl mul b) [:: ys; xs])). have [m Hm] : exists m : M _, iperm [:: xs; ys] = Ret [:: ys; xs] [~] m. have [m Hm] := @iperm_is_alt_ret M _ [:: ys; xs]. by exists m; rewrite -Hm /= !bindretf !insertE !fmapE !bindretf /= altC. by rewrite (lemma45b idempotent_converse injective_return H Hm). by rewrite /= -xxs -yys -(theorem46lid idempotent_converse injective_return yys). Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib