proposition: Lemma eval_itr e: eval (itr e) ≡ (eval e)^+.
proof: Proof. rewrite itr_str_l. destruct e as [n u M v]. change (mx_scal (u ⋅ (M + v ⋅ u) ^* ⋅ v) ≡ mx_scal (u ⋅ M ^* ⋅ v) ⋅ (mx_scal (u ⋅ M ^* ⋅ v))^*). rewrite <-mx_scal_str, <-mx_scal_dot. apply mx_scal_weq. rewrite str_pls. rewrite <-3dotA, <-str_dot. ra. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation