proposition: Lemma eval_dot e f: eval (dot 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 0 ⋅ (blk_mx M (v ⋅ s) 0 N)^* ⋅ col_mx 0 t) ≡ mx_scal (u ⋅ M ^* ⋅ v) ⋅ mx_scal (s ⋅ N ^* ⋅ t)). rewrite <-mx_scal_dot. apply mx_scal_weq. rewrite mx_str_trigonal. setoid_rewrite mx_dot_rowcol. rewrite dotplsx. rewrite <-dotA, mx_dot_rowcol. ra. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation