proposition: Lemma col_mx_leq_iff `{L: lattice.laws} n1 n2 m M1 M2 N1 N2: @col_mx X n1 n2 m M1 M2 ≦ col_mx N1 N2 <-> M1 ≦N1 /\ M2 ≦N2.
proof: Proof. split. unfold col_mx. intro H. split; intros i j. generalize (H (lshift i) j). now rewrite split_lshift. generalize (H (rshift i) j). now rewrite split_rshift. intros [? ?]. now apply col_mx_leq. Qed.
imports: comparisons kleene sums normalisation