proposition: Lemma epsilon_mx_pure n m (M: rmx n m): is_pure_mx M -> epsilon_mx M ≡ 0.
proof: Proof. intros HM i j. unfold epsilon_mx, mx_map. rewrite epsilon_pure. reflexivity. apply HM. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation