proposition: Lemma eval_pls e f: eval (pls e f) ≡ eval e + eval f.
proof: Proof. destruct e as [n u M v]. destruct f as [m s N t]. change (mx_scal (row_mx u s ⋅ (blk_mx M 0 0 N)^* ⋅ col_mx v t) ≡ mx_scal (u ⋅ M ^* ⋅ v) + mx_scal (s ⋅ N ^* ⋅ t)). rewrite <-mx_scal_pls. apply mx_scal_weq. rewrite mx_str_diagonal. setoid_rewrite mx_dot_rowcol. rewrite dotplsx. rewrite <-2dotA, 2mx_dot_rowcol. ra. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation