fact: Definition mx_blocks (M: MX x y) (N: MX x m) (P: MX n y) (Q: MX n m): MX (x+n) (y+m) := box _ _ (fun i j => match S i-x, S j-y with | O, O => !M i j | S i, O => !P i j | O, S j => !N i j | S i, S j => !Q i j end).
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)