proposition: Lemma square_triangular_blocks n m (M: MX n n) (N: MX n m) (P: MX m m): mx_blocks M N 0 P * mx_blocks M N 0 P == mx_blocks (M*M) (M*N+N*P) 0 (P*P).
proof: Proof. intros. rewrite mx_blocks_dot. apply mx_blocks_compat; semiring_reflexivity. Qed.
imports: ATBR(ATBR)