refactor(tactic/norm_num): define prove_ne_zero using prove_ne (#4626)

This is trickier than it sounds because of a cyclic dependency. As a result we
now have two versions of `prove_ne_zero` and `prove_clear_denom` is
generic over them. One version proves ne using an order relation on the
target, while the other uses `uncast` lemmas to reduce to `rat` and
then uses the first `prove_ne_zero`. (This is why we actually want two versions -
we can't solve this with a large mutual def, because it would
result in an infinite recursion.)