proposition: Lemma blk_mx' `{L: lattice.laws} {n1 n2 m1 m2} A B C D: @blk_mx X n1 n2 m1 m2 A B C D ≡ row_mx (col_mx A C) (col_mx B D).
proof: Proof. intros i j. unfold blk_mx, row_mx, col_mx. case split; case split; intros; reflexivity. Qed.
imports: comparisons kleene sums normalisation