proposition: Lemma mx_forall_blk f n1 n2 m1 m2 M11 M12 M21 M22: mx_forall f M11 -> mx_forall f M12 -> mx_forall f M21 -> mx_forall f M22 -> mx_forall f (@blk_mx _ n1 n2 m1 m2 M11 M12 M21 M22).
proof: Proof. intros. now apply mx_forall_col; apply mx_forall_row. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation