proposition: Lemma mx_blocks_star_trigonal n m (M: MX n n) (N: MX m m) (P: MX n m): (mx_blocks M P 0 N)# == mx_blocks (M#) (M# * P * N#) 0 (N#).
proof: Proof. intros. rewrite mx_blocks_star. apply mx_blocks_compat. apply star_compat. semiring_reflexivity. rewrite dot_ann_right, plus_neutral_right. trivial with algebra. semiring_reflexivity. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)