proposition: Lemma to_row_mx `{L: lattice.laws} {n m1 m2} (M: mx X n (m1+m2)): M ≡ row_mx (lsub_mx M) (rsub_mx M).
proof: Proof. intros i j. unfold row_mx, lsub_mx, rsub_mx. now case split_spec; intros i' ->. Qed.
imports: comparisons kleene sums normalisation