Going through a trivial exercise from Adam’s book but my proof general can’t find the tactic crush:
Error: The reference crush was not found in the current environment.
Why? And how do I put it in?
Module nn. Theorem add_induct2: forall n, n+0 = n. Proof. induction n; crush. End nn.