proposition: Lemma mx_dot_colrow n1 n2 m p1 p2 (M1: mx n1 m) (M2: mx n2 m) (N1: mx m p1) (N2: mx m p2): col_mx M1 M2 ⋅ row_mx N1 N2 ≡ blk_mx (M1⋅N1) (M1⋅N2) (M2⋅N1) (M2⋅N2).
proof: Proof. now rewrite mx_dot_colx, 2mx_dot_xrow. Qed.
imports: comparisons kleene sums normalisation