proposition: Lemma R_v: R ⋅ A^v ≦ B^v.
proof: Proof. intros j i'. apply leq_supx. intros i _. unfold dot; simpl. clear i'. match goal with [|- ?P (_ ?x ?y) ?z ] => change (leq (x ⋅ y) z) end. setoid_rewrite <-andb_dot. apply ofbool_leq. unfold leq;simpl; unfold le_bool. setoid_rewrite Bool.andb_true_iff. setoid_rewrite is_true_sumbool. now intros [H H0%(H nil)]. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation