proposition: Lemma col_mx_cup `{L: lattice.laws} n1 n2 m M M' N N': @col_mx X n1 n2 m (M ⊔ M') (N ⊔ N') ≡ col_mx M N ⊔ col_mx M' N'.
proof: Proof. intros i j. unfold col_mx. simpl. case split; reflexivity. Qed.
imports: comparisons kleene sums normalisation