feat(tactic/qify) : `qify` tactic (#16313)
This file mainly introduces `qify` which casts goals or hypotheses about natural numbers or integers to the ones about rational numbers.
Note that this file is following from `zify`.
This is motivated by thinking about division in natural numbers or integers. Division in natural numbers or integers is not always working fine (e.g. (5 : ℕ) / 2 = 2), so it's easier to work in `ℚ`, where division and subtraction are well behaved.
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
