proposition: Lemma mx_dot_neutral_left n m (M: MX n m): 1 * M == M.
proof: Proof. intros i j Hi Hj. simpl. rewrite (sum_cut_nth i) by auto with arith; simpl. transitivity (0 + !M i j + 0); [|semiring_reflexivity]. repeat apply plus_compat; try (apply sum_zero; intros); nat_analyse; semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(BoolView)