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