proposition: Lemma mx_star_make_left n: forall M: MX n n, 1 + M# * M == M#.
proof: Proof. unfold star, mx_Star_Op. induction n; intro M. mx_intros i j Hi Hj. Opaque one dot plus. simpl. Transparent one dot plus. change (S n) with (1+n)%nat. apply build_star_make_left. intro N; mx_intros i j Hi Hj. unfold mx_to_scal. simpl. rewrite <- star_make_left at 2. semiring_reflexivity. exact IHn. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)