proposition: Lemma mx_point_dot n m o i j k: forall a b: X A A, j < m -> mx_point n m i j a * mx_point m o j k b == mx_point n o i k (a*b).
proof: Proof. repeat intro; simpl. rewrite (sum_cut_nth j) by assumption. rewrite 2sum_zero; intros. nat_analyse; simpl; semiring_reflexivity. nat_analyse; simpl; trivial with algebra. nat_analyse; simpl; trivial with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(BoolView)