proposition: Lemma mx_transpose_blocks x y n m (a: MX x y) b c (d: MX n m): mx_transpose (mx_blocks a b c d) == mx_blocks (mx_transpose a) (mx_transpose c) (mx_transpose b) (mx_transpose d).
proof: Proof. repeat intro. simpl. destruct_blocks; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)