proposition: Lemma mx_lsub_row `{lattice.laws} n m1 m2 M1 M2: lsub_mx (@row_mx X n m1 m2 M1 M2) ≡ M1.
proof: Proof. intros i j. unfold lsub_mx, row_mx. now rewrite split_lshift. Qed.
imports: kleene normalisation ordinal sups matrix