proposition: Lemma mx_point_one_left n m p i j: forall M: MX m p, j < m -> mx_point n m i j 1 * M == box n p (fun s t => xif (eq_nat_bool i s) (!M j t) 0).
proof: Proof. intros. unfold mx_point. mx_intros s t Hs Ht. simpl. rewrite (sum_cut_nth j) by auto. rewrite 2 sum_zero; intros; nat_analyse; simpl; semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(BoolView)