proposition: Lemma mx_point_center n m p q i j (M: MX n m) (N: MX p q): i < m -> j < p -> M * mx_point m p i j 1 * N == box n q (fun s t => !M s i * !N j t).
proof: Proof. intros Hi Hj x y Hx Hy. simpl. setoid_rewrite sum_distr_left. rewrite (sum_cut_nth j);auto. rewrite sum_zero. rewrite (sum_cut_nth i). setoid_rewrite sum_zero; intros; simpl; nat_analyse; simpl; try semiring_reflexivity. rewrite sum_zero. reflexivity. intros. bool_simpl; simpl. semiring_reflexivity. auto. intros. rewrite sum_zero. reflexivity. 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)