proposition: Lemma itr_aea `{laws} `{STR ≪ l} n (a e: X n n): a⋅a ≡a -> (a⋅e)^+⋅a ≡ (a⋅e⋅a)^+.
proof: Proof. intro Ha. rewrite (itr_str_l (a⋅e⋅a)), <-dotA, str_dot, (dotA a a), Ha. now rewrite dotA, <-itr_str_l. Qed.
imports: monoid