can you use the Nat solver in agda-stdlib for proof by contradiction? In particular I have a gnarly bit of algebra I'd rather not do by hand, but I'm not sure how to use a solver to make my life easier. For reference this is the result I want to prove:
{n m : ℕ} → 3 + (n + (3 + (n + (3 + (n + n * (3 + n)))))) ≡ 1 + m + (1 + m + (1 + m + 0)) + 2 → ⊥