proposition: Lemma mx_dot_assoc n m p o (M: MX n m) (N: MX m p) (P: MX p o): M*(N*P) == (M*N)*P.
proof: Proof. intros i j Hi Hj. simpl. transitivity (sum 0 m (fun k => sum 0 p (fun k' => !M i k * !N k k' * !P k' j))). apply sum_compat; intros. rewrite sum_distr_right; auto with algebra. rewrite sum_inversion. apply sum_compat; intros. rewrite sum_distr_left; auto with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(BoolView)