proposition: Lemma str_dot_refl `{laws} `{KA ≪ l} n (x y: X n n): 1 ≦x -> 1 ≦y -> (x⋅y)^* ≡ (x+y)^*.
proof: Proof. intros Hx Hy. apply antisym. - apply str_ind_l1. apply str_refl. rewrite <-2str_cons at 2. rewrite dotA. repeat apply dot_leq; lattice. - apply str_ind_l1. apply str_refl. rewrite <-str_cons at 2. apply dot_leq. 2: reflexivity. apply leq_cupx. now rewrite <-Hy, dotx1. now rewrite <-Hx, dot1x. Qed.
imports: monoid