proposition: Lemma str_move_l `{laws} `{STR ≪ l} n m (x: X n m) y z: x ⋅ y ≦ z ⋅ x -> x ⋅ y^* ≦ z^* ⋅ x.
proof: Proof. intro E. apply str_ind_r'. now rewrite <-str_refl, dot1x. rewrite <-str_snoc at 2. now rewrite <-dotA, E, dotA. Qed.
imports: monoid