proposition: Lemma flatten_aux_valid `(M: @EMonoid A op one eqv): forall t t', (eval M t * eval M t')%M == (eval M (flatten_aux t t')).
proof: Proof. add_op_proper M HM. induction t;simpl. - intro t'; rewrite <- IHt1; rewrite <- IHt2; monoid_simpl M;reflexivity. - intro t';monoid_simpl M; reflexivity. - reflexivity. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)