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