Assume the Necessitation Rule and the Distribution Axiom (https://en.wikipedia.org/wiki/Modal_logic#Axiomatic_systems) of modal logic, and also assume the axiom $p\land \diamond q\to \diamond(q\land\diamond p)$. Suppose that $\neg(\diamond p\land q) $ is provable (one can apply all standard inference rules and all tautologies of propositional logic). I'm trying to show that $\neg (p\land \diamond q)$ is also provable.
Assume by contradiction $p\land \diamond q$. By modus ponens, $\diamond(q\land\diamond p)$ or $\neg \square \neg (q\land \diamond p)$. We also have $\neg (q \land \diamond p)$. But I don't see how to obtain a contradiction.