proposition: Lemma mx_forall_row f n m1 m2 M11 M21: mx_forall f M11 -> mx_forall f M21 -> mx_forall f (@row_mx _ n m1 m2 M11 M21).
proof: Proof. repeat intro. unfold row_mx. now case ordinal.split. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation