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