proposition: Lemma str_move `{laws} `{STR ≪ l} n m (x: X n m) y z: x ⋅ y ≡ z ⋅ x -> x ⋅ y^* ≡ z^* ⋅ x.
proof: Proof. intro. apply antisym. apply str_move_l. now apply weq_leq. apply str_move_r. now apply weq_geq. Qed.
imports: monoid