a✝ b c a : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
d0 : 0 < ↑d
⊢ Rat.Nonneg (n /. ↑d) → Rat.Nonneg (-(n /. ↑d)) → n /. ↑d = 0
a✝ b c a : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ Rat.Nonneg (n /. ↑d) → Rat.Nonneg (-(n /. ↑d)) → n /. ↑d = 0
have d0 : 0 < (d : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h)
a✝ b c a : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
d0 : 0 < ↑d
⊢ 0 ≤ n → n ≤ 0 → n = 0
a✝ b c a : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
d0 : 0 < ↑d
⊢ Rat.Nonneg (n /. ↑d) → Rat.Nonneg (-(n /. ↑d)) → n /. ↑d = 0
rw [divInt_nonneg _ d0, neg_def, divInt_nonneg _ d0, Right.nonneg_neg_iff,
  divInt_eq_zero d0.ne.symm]
no goals
a✝ b c a : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
d0 : 0 < ↑d
⊢ 0 ≤ n → n ≤ 0 → n = 0
exact fun h₁ h₂ => le_antisymm h₂ h₁