proposition: Lemma mx_star_block_destruct_left: forall x n m (M: MX (x+n) (x+n)) (Y: MX (x+n) m), M * Y <== Y -> mx_star_block M * Y <== Y.
proof: Proof. intros x n m. apply build_star_destruct_left; intros ? ? ?; apply mx_star_destruct_left. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)