proposition: Lemma itr_move `{laws} `{STR ≪ l} n (x: X n n): x ⋅ x^* ≡ x^* ⋅ x.
proof: Proof. apply antisym. rewrite <-dot1x, (str_refl x), dotA. apply str_ind_r. now rewrite str_snoc at 1. apply str_ind_l'. now rewrite <-str_refl, dotx1. now rewrite str_cons at 1. Qed.
imports: lattice