proposition: Lemma itr_pls_itr `{laws} `{KA ≪ l} n (x y: X n n): (x+y)^+ ≡ (x^+ + y^+)^+.
proof: Proof. apply antisym. apply itr_leq. now rewrite <-2itr_ext. apply itr_ind_l1. apply leq_cupx; apply itr_leq; lattice. rewrite dotplsx. apply leq_cupx; apply itr_ind_l; rewrite <-itr_cons at 2; apply dot_leq; lattice. Qed.
imports: monoid