Computing with polynomials

Stream: new members

[Amos Turchet]

I'm trying to prove the following lemma about lower bound for the value of a polynomial with integral coefficients evaluated at a rational number at a rational which is not a root of the polynomial. And I'm getting stuck and a bit worried:

import data.polynomial
import data.rat
notation α`[X]` := polynomial α
/-
 The Lemma gives a lower bound on the absolute value of a polynomial f with integral coefficients evaluated at a rational number q which is not a root of f
 -/
lemma poly_not_zero_low_bound (x : ℚ) (p : ℤ [X]) (hx : x.denom > 0) (hpx : polynomial.aeval x p ≠ 0) : abs(polynomial.aeval x p) ≥ 1 / (x.denom)^(p.nat_degree) :
begin
  calc abs(polynomial.aeval x p) = abs((polynomial.aeval x p).num / (polynomial.aeval x p).denom) : by rw rat.num_denom (polynomial.aeval x p)
  ... = abs(polynomial.aeval x p).num / abs(polynomial.aeval x p).denom : by rw abs_div
  ... ≥ 1 / (abs(polynomial.aeval x p)).denom : by sorry --rw [hx, rat.mk_eq_zero, int.nat_abs_ne_zero_of_ne_zero]
  ... ≥ 1 / (x.denom)^(p.nat_degree) : by sorry
end

This was proven (a bit more generally) by @Jujian Zhang and it takes more than 100 lines of codes. To me it seems that the only actual computation to be done should be the last step which ideally would take less than that.
But before that it looks like I have issues with using rat.num_denom as well as showing that given hpx the numerator is a non-zero integer and therefore its absolute value is at least 1 (what David Masser calls the "Fundamental Theorem of Trascendence").