proposition: Lemma mx_decompose_blocks : forall M: MX (x+n) (y+m), M == mx_blocks (mx_sub00 M) (mx_sub01 M) (mx_sub10 M) (mx_sub11 M).
proof: Proof. simpl; intros. destruct_blocks; auto with lia. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)