proposition: Lemma is_01_mx_dot n m p (M: rmx n m) (N: rmx m p): is_01_mx M -> is_01_mx N -> is_01_mx (M⋅N).
proof: Proof. repeat intro. apply is_01_sup. now constructor. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation