proposition: Lemma itr_move `{laws} `{STR ≪ l} n m (x: X n m) y z: x ⋅ y ≡ z ⋅ x -> x ⋅ y^+ ≡ z^+ ⋅ x.
proof: Proof. intro E. rewrite itr_str_l, dotA, E, <-dotA, str_move by eassumption. now rewrite dotA, <-itr_str_l. Qed.
imports: monoid