proposition: Lemma deriv_eval a n u (M: rmx n n) v: is_01_mx u -> is_pure_mx M -> is_01_mx v -> deriv a (mx_scal (u⋅M^*⋅v)) ≡ mx_scal (u⋅epsilon_mx (deriv_mx a M)⋅M^*⋅v).
proof: Proof. intros Hu HM Hv. rewrite (scal_mx_map (deriv a)). apply mx_scal_weq. rewrite 2deriv_mx_dot, deriv_mx_str_strict. 2: apply epsilon_mx_pure; assumption. rewrite <-expand_01_mx by assumption. rewrite (deriv_01_mx _ Hu), (deriv_01_mx _ Hv), epsilon_deriv_pure_mx by assumption. ra. Qed.
imports: positives comparisons kleene regex rmx sums matrix_ext prop normalisation