proposition: Lemma mx_star_compat n (M N: MX n n): M==N -> M# == N# .
proof: Proof. unfold star, mx_Star_Op. induction n; intro. assumption. Opaque equal. cbn. change (S n) with (1+n)%nat. auto 13 with compat. Transparent equal. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)