proposition: Theorem morphism_distribution: forall {M N: Type} `{MM: Monoid M} `{MN: Monoid N} `{CMM: @ChunkableMonoid N MN} (f: N -> M) `{MMf: @MonoidMorphism _ _ MN MM f}, forall i x, f x = mconcat (map f (chunk i x)).
proof: Proof. intros. funelim (chunk i x). { simpl. simp mconcat. now rewrite monoid_right_identity. } simpl. simp mconcat. rewrite <- H; auto. rewrite <- morphism_op. now rewrite <- take_drop_spec. Qed.
imports: Arith Coq.Classes.DecidableClass Coq.Program.Wf List Lia PeanoNat Program Equations(Equations)