fix(tactic/norm_num): workaround int.sub unfolding bug (#2804)
Fixes https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/certificates.20for.20calculations/near/198631936 . Or rather, it works around an issue in how the kernel unfolds applications. The real fix is probably to adjust the definitional height or other heuristics around `add_group_has_sub` and `int.sub` so that tries to prove that they are defeq that way rather than unfolding `bit0` and `bit1`. Here is a MWE for the issue:
```lean
example : int.has_sub = add_group_has_sub := rfl
example :
(@has_sub.sub ℤ int.has_sub 5000 2 : ℤ) =
(@has_sub.sub ℤ add_group_has_sub 5000 2) := rfl -- deep recursion
```
Co-authored-by: Scott Morrison <scott@tqft.net>
