proposition: Lemma R_u: A^u ≦ B^u ⋅ R.
proof: Proof. intros z i. cbn. rewrite mx_dot_fun, dot1x. unfold mx_fun. clear z. case eqb_ord_spec. 2: intro; apply leq_bx. intros ->. apply epsilon_reflexive. unfold R. rewrite sumbool_true. reflexivity. rewrite <-2dfa.eval_lang, <-2dfa.reroot_id. exact HAB. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation