proposition: Lemma mx_dot_blk n1 n2 m1 m2 p1 p2 (M11: mx n1 m1) (M12: mx n1 m2) (M21: mx n2 m1) (M22: mx n2 m2) (N11: mx m1 p1) (N12: mx m1 p2) (N21: mx m2 p1) (N22: mx m2 p2): blk_mx M11 M12 M21 M22 ⋅ blk_mx N11 N12 N21 N22 ≡ blk_mx (M11⋅N11+M12⋅N21) (M11⋅N12+M12⋅N22) (M21⋅N11+M22⋅N21) (M21⋅N12+M22⋅N22).
proof: Proof. setoid_rewrite blk_mx' at 2. setoid_rewrite mx_dot_colrow. now rewrite 4mx_dot_rowcol. Qed.
imports: comparisons kleene sums normalisation