proposition: Lemma mx_point_blocks10 n m x y: forall i j (a: X A A), n<=i -> j<m -> mx_point (n+x) (m+y) i j a == mx_blocks 0 0 (mx_point x m (i-n) j a) 0.
proof: Proof. simpl; intros. destruct_blocks; nat_analyse; trivial. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(MxGraph) ATBR(SemiLattice) ATBR(BoolView)