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