proposition: Lemma mx_point_dot_zero n m o i j j' k: forall a b: X A A, j<>j' -> mx_point n m i j a * mx_point m o j' k b == 0.
proof: Proof. repeat intro; simpl. apply sum_zero. intros. 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)