proposition: Lemma det_MX: X ⋅ M^* ≡ det^M^* ⋅ X.
proof: Proof. apply str_move. rewrite M_sum. cbn. rewrite dotxsum, dotsumx. apply sup_weq. 2: reflexivity. intros a x j. rewrite mx_dot_fun. unfold X. rewrite (mem_of_row ord0) by (unfold T_; auto with mx_predicates). unfold weq. setoid_rewrite dotxsum. apply sup_weq. 2: reflexivity. intro j'. unfold M_, T_, epsilon_mx, mx_map. now rewrite 2dotA, dot_ofboolx. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation