[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
⊢ Rat.floor a = a.num / ↑a.den
[PROOFSTEP]
rw [Rat.floor]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
⊢ (if a.den = 1 then a.num else a.num / ↑a.den) = a.num / ↑a.den
[PROOFSTEP]
split
[GOAL]
case inl
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : a.den = 1
⊢ a.num = a.num / ↑a.den
[PROOFSTEP]
next h => simp [h]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h : a.den = 1
⊢ a.num = a.num / ↑a.den
[PROOFSTEP]
simp [h]
[GOAL]
case inr
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
[PROOFSTEP]
next => rfl
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
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
[PROOFSTEP]
simp [Rat.floor_def']
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ n / ↑d ↔ ↑z ≤ mk' n d
[PROOFSTEP]
rw [num_den']
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
[PROOFSTEP]
have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h)
[GOAL]
α : Type u_1
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
[PROOFSTEP]
conv =>
  rhs
  rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
[GOAL]
α : Type u_1
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
[PROOFSTEP]
  rhs
  rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
[GOAL]
α : Type u_1
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
[PROOFSTEP]
  rhs
  rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
[GOAL]
α : Type u_1
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
[PROOFSTEP]
rhs
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
| ↑z ≤ n /. ↑d
[PROOFSTEP]
rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
[GOAL]
α : Type u_1
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
[PROOFSTEP]
exact Int.le_ediv_iff_mul_le h'
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
⊢ ⌊↑n / ↑d⌋ = n / ↑d
[PROOFSTEP]
rw [Rat.floor_def]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
[PROOFSTEP]
obtain rfl | hd := @eq_zero_or_pos _ _ d
[GOAL]
case inl
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
⊢ (↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
[PROOFSTEP]
set q := (n : ℚ) / d with q_eq
[GOAL]
case inr
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ q.num / ↑q.den = n / ↑d
[PROOFSTEP]
obtain ⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩ : ∃ c, n = c * q.num ∧ (d : ℤ) = c * q.den :=
  by
  rw [q_eq]
  exact_mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (by exact_mod_cast hd.ne')
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * q.num ∧ ↑d = c * ↑q.den
[PROOFSTEP]
rw [q_eq]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den
[PROOFSTEP]
exact_mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (by exact_mod_cast hd.ne')
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ↑d ≠ 0
[PROOFSTEP]
exact_mod_cast hd.ne'
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = n / ↑d
[PROOFSTEP]
rw [n_eq_c_mul_num, d_eq_c_mul_denom]
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = c * q.num / (c * ↑q.den)
[PROOFSTEP]
refine' (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left _ <| Int.coe_nat_nonneg q.den).symm
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < c * ↑q.den
[PROOFSTEP]
rwa [← d_eq_c_mul_denom, Int.coe_nat_pos]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ↑⌊x⌋ ≤ ↑x ∧ ↑x < ↑⌊x⌋ + 1
[PROOFSTEP]
exact_mod_cast floor_eq_iff.1 (Eq.refl ⌊x⌋)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ⌈↑x⌉ = ⌈x⌉
[PROOFSTEP]
rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ round ↑x = round x
[PROOFSTEP]
have H : ((2 : ℚ) : α) = (2 : α) := Rat.cast_coe_nat 2
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
⊢ round ↑x = round x
[PROOFSTEP]
have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp [H]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
⊢ ↑(x + 1 / 2) = ↑x + 1 / 2
[PROOFSTEP]
simp [H]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ round ↑x = round x
[PROOFSTEP]
rw [round_eq, round_eq, ← this, floor_cast]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ↑(fract x) = fract ↑x
[PROOFSTEP]
simp only [fract, cast_sub, cast_coe_int, floor_cast]
[GOAL]
n : ℤ
d : ℕ
⊢ n % ↑d = n - ↑d * ⌊↑n / ↑d⌋
[PROOFSTEP]
rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_int_div_nat_eq_div]
[GOAL]
n d : ℕ
n_coprime_d : coprime n d
⊢ coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
[PROOFSTEP]
have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div
[GOAL]
n d : ℕ
n_coprime_d : coprime n d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
[PROOFSTEP]
rw [← this]
[GOAL]
n d : ℕ
n_coprime_d : coprime n d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ coprime (natAbs (↑n % ↑d)) d
[PROOFSTEP]
have : d.coprime n := n_coprime_d.symm
[GOAL]
n d : ℕ
n_coprime_d : coprime n d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : coprime d n
⊢ coprime (natAbs (↑n % ↑d)) d
[PROOFSTEP]
rwa [Nat.coprime, Nat.gcd_rec] at this 
[GOAL]
q : ℚ
⊢ q.num < (⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den by exact_mod_cast this
[GOAL]
q : ℚ
this : ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
⊢ q.num < (⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
exact_mod_cast this
[GOAL]
q : ℚ
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
suffices (q.num : ℚ) < (q - fract q + 1) * q.den
  by
  have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
  rwa [this]
[GOAL]
q : ℚ
this : ↑q.num < (q - fract q + 1) * ↑q.den
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
[GOAL]
q : ℚ
this✝ : ↑q.num < (q - fract q + 1) * ↑q.den
this : ↑⌊q⌋ = q - fract q
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
rwa [this]
[GOAL]
q : ℚ
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
[PROOFSTEP]
suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den
  by
  have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den
  calc
    (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
    _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
    _ = q.num + (1 - fract q) * q.den := by simp
  rwa [this]
[GOAL]
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
[PROOFSTEP]
have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den
[GOAL]
case this
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
q : ℚ
this✝ : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
this : (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
[PROOFSTEP]
calc
  (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
  _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
  _ = q.num + (1 - fract q) * q.den := by simp
[GOAL]
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = (q + (1 - fract q)) * ↑q.den
[PROOFSTEP]
ring
[GOAL]
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q + (1 - fract q)) * ↑q.den = q * ↑q.den + (1 - fract q) * ↑q.den
[PROOFSTEP]
rw [add_mul]
[GOAL]
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ q * ↑q.den + (1 - fract q) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
[PROOFSTEP]
simp
[GOAL]
q : ℚ
this✝ : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
this : (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
[PROOFSTEP]
rwa [this]
[GOAL]
q : ℚ
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
[PROOFSTEP]
suffices 0 < (1 - fract q) * q.den by
  rw [← sub_lt_iff_lt_add']
  simpa
[GOAL]
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
[PROOFSTEP]
rw [← sub_lt_iff_lt_add']
[GOAL]
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num - ↑q.num < (1 - fract q) * ↑q.den
[PROOFSTEP]
simpa
[GOAL]
q : ℚ
⊢ 0 < (1 - fract q) * ↑q.den
[PROOFSTEP]
have : 0 < 1 - fract q := by
  have : fract q < 1 := fract_lt_one q
  have : 0 + fract q < 1 := by simp [this]
  rwa [lt_sub_iff_add_lt]
[GOAL]
q : ℚ
⊢ 0 < 1 - fract q
[PROOFSTEP]
have : fract q < 1 := fract_lt_one q
[GOAL]
q : ℚ
this : fract q < 1
⊢ 0 < 1 - fract q
[PROOFSTEP]
have : 0 + fract q < 1 := by simp [this]
[GOAL]
q : ℚ
this : fract q < 1
⊢ 0 + fract q < 1
[PROOFSTEP]
simp [this]
[GOAL]
q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 < 1 - fract q
[PROOFSTEP]
rwa [lt_sub_iff_add_lt]
[GOAL]
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * ↑q.den
[PROOFSTEP]
exact mul_pos this (by exact_mod_cast q.pos)
[GOAL]
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < ↑q.den
[PROOFSTEP]
exact_mod_cast q.pos
[GOAL]
q : ℚ
q_pos : 0 < q
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
have q_num_pos : 0 < q.num := Rat.num_pos_iff_pos.mpr q_pos
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
have q_num_abs_eq_q_num : (q.num.natAbs : ℤ) = q.num := Int.natAbs_of_nonneg q_num_pos.le
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
set q_inv := (q.den : ℚ) / q.num with q_inv_def
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
have q_inv_eq : q⁻¹ = q_inv := Rat.inv_def''
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
suffices (q_inv - ⌊q_inv⌋).num < q.num by rwa [q_inv_eq]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : (q_inv - ↑⌊q_inv⌋).num < q.num
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
rwa [q_inv_eq]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ (q_inv - ↑⌊q_inv⌋).num < q.num
[PROOFSTEP]
suffices ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num < q.num by field_simp [this, ne_of_gt q_num_pos]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
⊢ (q_inv - ↑⌊q_inv⌋).num < q.num
[PROOFSTEP]
field_simp [this, ne_of_gt q_num_pos]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
[PROOFSTEP]
suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
  -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
  have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ :=
    by
    suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.coprime q.num.natAbs by
      exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
    have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
    simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
  rwa [this]
    -- to show the claim, start with the following inequality
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
[PROOFSTEP]
have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ :=
  by
  suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.coprime q.num.natAbs by
    exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
  have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
  simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
[PROOFSTEP]
suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.coprime q.num.natAbs by
  exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this✝ : ↑q.den - q.num * ⌊q_inv⌋ < q.num
this : Nat.coprime (natAbs (↑q.den - q.num * ⌊q_inv⌋)) (natAbs q.num)
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
[PROOFSTEP]
exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
⊢ Nat.coprime (natAbs (↑q.den - q.num * ⌊q_inv⌋)) (natAbs q.num)
[PROOFSTEP]
have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
tmp : Nat.coprime (natAbs (↑q.den - ↑(natAbs q.num) * ⌊↑q.den / ↑(natAbs q.num)⌋)) (natAbs q.num)
⊢ Nat.coprime (natAbs (↑q.den - q.num * ⌊q_inv⌋)) (natAbs q.num)
[PROOFSTEP]
simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this✝ : ↑q.den - q.num * ⌊q_inv⌋ < q.num
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
[PROOFSTEP]
rwa [this]
  -- to show the claim, start with the following inequality
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
[PROOFSTEP]
have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den :=
  by
  have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
  have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this 
  rwa [← sub_lt_iff_lt_add'] at this 
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
[PROOFSTEP]
have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
[PROOFSTEP]
have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this 
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
⊢ q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
[PROOFSTEP]
rwa [right_distrib, one_mul] at this 
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this✝ : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
this : q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
[PROOFSTEP]
rwa [← sub_lt_iff_lt_add'] at this 
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
[PROOFSTEP]
have : q_inv.num = q.den ∧ q_inv.den = q.num.natAbs :=
  by
  have coprime_q_denom_q_num : q.den.coprime q.num.natAbs := q.reduced.symm
  have : Int.natAbs q.den = q.den := by simp
  rw [← this] at coprime_q_denom_q_num 
  rw [q_inv_def]
  constructor
  · exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
  · suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact_mod_cast this
    rw [q_num_abs_eq_q_num]
    exact_mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
[PROOFSTEP]
have coprime_q_denom_q_num : q.den.coprime q.num.natAbs := q.reduced.symm
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime q.den (natAbs q.num)
⊢ q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
[PROOFSTEP]
have : Int.natAbs q.den = q.den := by simp
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime q.den (natAbs q.num)
⊢ natAbs ↑q.den = q.den
[PROOFSTEP]
simp
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime q.den (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
[PROOFSTEP]
rw [← this] at coprime_q_denom_q_num 
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
[PROOFSTEP]
rw [q_inv_def]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ (↑q.den / ↑q.num).num = ↑q.den ∧ (↑q.den / ↑q.num).den = natAbs q.num
[PROOFSTEP]
constructor
[GOAL]
case left
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ (↑q.den / ↑q.num).num = ↑q.den
[PROOFSTEP]
exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
[GOAL]
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ (↑q.den / ↑q.num).den = natAbs q.num
[PROOFSTEP]
suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact_mod_cast this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this✝ : natAbs ↑q.den = q.den
this : ↑(↑q.den / ↑q.num).den = ↑(natAbs q.num)
⊢ (↑q.den / ↑q.num).den = natAbs q.num
[PROOFSTEP]
exact_mod_cast this
[GOAL]
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ ↑(↑q.den / ↑q.num).den = ↑(natAbs q.num)
[PROOFSTEP]
rw [q_num_abs_eq_q_num]
[GOAL]
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ ↑(↑q.den / ↑q.num).den = q.num
[PROOFSTEP]
exact_mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
this : q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
[PROOFSTEP]
rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq 
