proposition: Lemma str_pls `{laws} `{KA ≪ l} n (x y: X n n): (x+y)^* ≡ x^*⋅(y⋅x^*)^*.
proof: Proof. apply str_unique. rewrite <-2str_refl. now rewrite dotx1. rewrite dotplsx. apply leq_cupx. now rewrite dotA, str_cons. rewrite <-(str_refl x) at 3. now rewrite dot1x, dotA, str_cons. intros z Hz. rewrite dotplsx in Hz. apply cup_spec in Hz as [Hxz Hyz]. rewrite <-dotA. apply str_ind_l'. 2: assumption. apply str_ind_l. rewrite <- Hyz at 2. rewrite <-dotA. apply dot_leq. reflexivity. now apply str_ind_l. Qed.
imports: monoid