proposition: Lemma mx_blocks_star': forall x n (M: MX (x+n) (x+n)), M# == mx_star_block M.
proof: Proof. intros. apply leq_antisym. apply star_destruct_right_one. rewrite mx_star_block_make_left. reflexivity. rewrite <- (dot_neutral_right (mx_star_block M)). rewrite (one_leq_star_a M). apply mx_star_block_destruct_left. rewrite <- star_make_right at 2. auto with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)