proposition: Lemma commute_empty: Algebraic.empty [=0=] preNFA_to_preMAUT empty.
proof: Proof. constructor. mx_intros i j Hi Hj. simpl. fold_regex. case_eq (epsilonbrel empty (state_of_nat i) (state_of_nat j)); intro H. elim (epsilon_empty H). unfold labelling; simpl. fold_regex; semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)