proposition: Lemma epsilon_eval n u (M: rmx n n) v: is_pure_mx M -> (epsilon (mx_scal (u⋅M^*⋅v)) <-> epsilon (mx_scal (u⋅v))).
proof: Proof. intro HM. rewrite 2epsilon_iff_reflexive_eps. rewrite 2(scal_mx_map (fun e => eps e)). rewrite 3epsilon_mx_dot, epsilon_mx_str, (epsilon_mx_pure HM). now rewrite str0, dotx1. Qed.
imports: positives comparisons kleene regex rmx sums matrix_ext prop normalisation