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