proposition: Lemma mx_forall_col f n1 n2 m M11 M21: mx_forall f M11 -> mx_forall f M21 -> mx_forall f (@col_mx _ n1 n2 m M11 M21).
proof: Proof. repeat intro. unfold col_mx. now case ordinal.split. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation