proposition: Lemma deriv_mx_dot a n m p (M: rmx n m) (N: rmx m p): deriv_mx a (M⋅N) ≡ deriv_mx a M ⋅ N + epsilon_mx M ⋅ deriv_mx a N.
proof: Proof. intros i j. setoid_rewrite deriv_sup. simpl deriv; fold_regex. apply supcup. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation