proposition: Lemma to_blk_mx `{L: lattice.laws} {n1 n2 m1 m2} (M: mx X (n1+n2) (m1+m2)): M ≡ blk_mx (sub00_mx M) (sub01_mx M) (sub10_mx M) (sub11_mx M).
proof: Proof. rewrite to_row_mx at 1. rewrite to_col_mx. reflexivity. Qed.
imports: comparisons kleene sums normalisation