proposition: Lemma R_M: R ⋅ A^M^* ≦ B^M^* ⋅ R.
proof: Proof. apply str_move_l. setoid_rewrite dotxsum. setoid_rewrite dotsumx. apply sup_leq'. exact Hvars. intros a Ha j i'. apply leq_supx. intros i _. rewrite mx_dot_fun. setoid_rewrite <-dot_ofboolx. unfold mx_fun. case eqb_spec. 2: ra. intros ->. apply dot_leq. 2: reflexivity. apply ofbool_leq. unfold leq;simpl; unfold le_bool. setoid_rewrite is_true_sumbool. intros H w Hw. apply (H (cons a w)). now split. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation