proposition: Lemma dot_scal_left_blocks n m p q (N: MX n p) (M: MX n q) (P: MX m p) (Q: MX m q) x: x '* mx_blocks N M P Q == mx_blocks (x '* N) (x '* M) (x '* P) (x '* Q).
proof: Proof. repeat intro; simpl. destruct_blocks; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(BoolView)