proposition: Lemma mx_blocks_sum low up n m p q (a : nat -> MX n p) (b : nat -> MX n q) (c : nat -> MX m p) (d : nat -> MX m q): sum low up (fun u => mx_blocks (a u) (b u) (c u) (d u)) == mx_blocks (sum low up a) (sum low up b)(sum low up c)(sum low up d) .
proof: Proof. intros. induction up. simpl. intros. destruct_blocks; reflexivity. setoid_rewrite sum_enter_right. rewrite IHup. setoid_rewrite mx_blocks_plus. auto with compat. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)