α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ n / ↑d ↔ ↑z ≤ mk' n d
α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ Rat.floor (mk' n d) ↔ ↑z ≤ mk' n d
simp [Rat.floor_def']
α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ n / ↑d ↔ ↑z ≤ mk' n d
rw [num_den']
α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h)
α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ z * ↑d ≤ n
α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
conv =>
  rhs
  rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
no goals
α : Type ?u.897
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ z * ↑d ≤ n
exact Int.le_ediv_iff_mul_le h'