proposition: Lemma mx_tsub_col `{lattice.laws} n1 n2 m M1 M2: tsub_mx (@col_mx X n1 n2 m M1 M2) ≡ M1.
proof: Proof. intros i j. unfold tsub_mx, col_mx. now rewrite split_lshift. Qed.
imports: kleene normalisation ordinal sups matrix