proposition: Lemma to_col_mx `{L: lattice.laws} {n1 n2 m} (M: mx X (n1+n2) m): M ≡ col_mx (tsub_mx M) (bsub_mx M).
proof: Proof. intros i j. unfold col_mx, tsub_mx, bsub_mx. now case split_spec; intros i' ->. Qed.
imports: comparisons kleene sums normalisation