proposition: Lemma mx_vars_full n m (M: rmx n m) i j: vars (M i j) ≦ mx_vars M.
proof: Proof. unfold mx_vars. do 2 erewrite <-leq_xsup by apply in_seq. reflexivity. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation