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