/-
Copyright (c) 2019 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro, Kevin Kappelmann

! This file was ported from Lean 3 source module data.rat.floor
! leanprover-community/mathlib commit e1bccd6e40ae78370f01659715d3c948716e3b7e
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.Floor
import Mathlib.Algebra.EuclideanDomain.Instances
import Mathlib.Data.Rat.Cast
import Mathlib.Tactic.FieldSimp

/-!
# Floor Function for Rational Numbers

## Summary

We define the `FloorRing` instance on `ℚ`. Some technical lemmas relating `floor` to integer
division and modulo arithmetic are derived as well as some simple inequalities.

## Tags

rat, rationals, ℚ, floor
-/


open Int

namespace Rat

variable {α: Type ?u.3198
α : Type _: Type (?u.3373+1)
Type _} [LinearOrderedField: Type ?u.5 → Type ?u.5
LinearOrderedField α: Type ?u.897
α] [FloorRing: (α : Type ?u.3012) → [inst : LinearOrderedRing α] → Type ?u.3012
FloorRing α: Type ?u.2
α]

protected theorem floor_def': ∀ (a : ℚ), Rat.floor a = a.num / ↑a.den
floor_def' (a: ℚ
a : ℚ: Type
ℚ) : a: ℚ
a.floor: ℚ → ℤ
floor = a: ℚ
a.num: ℚ → ℤ
num / a: ℚ
a.den: ℚ → ℕ
den := by
Goals accomplished! 🐙
  α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

Rat.floor a = a.num / ↑a.denrw [α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

Rat.floor a = a.num / ↑a.denRat.floor: ℚ → ℤ
Rat.floorα: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

(if a.den = 1 then a.num else a.num / ↑a.den) = a.num / ↑a.den]α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

(if a.den = 1 then a.num else a.num / ↑a.den) = a.num / ↑a.den
  α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

Rat.floor a = a.num / ↑a.densplitα: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: a.den = 1

inla.num = a.num / ↑a.den
α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: ¬a.den = 1

inra.num / ↑a.den = a.num / ↑a.den
  α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

Rat.floor a = a.num / ↑a.den.α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: a.den = 1

inla.num = a.num / ↑a.den α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: a.den = 1

inla.num = a.num / ↑a.den
α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: ¬a.den = 1

inra.num / ↑a.den = a.num / ↑a.dennext h: a.den = 1
h => α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: a.den = 1

inla.num = a.num / ↑a.densimp [h: a.den = 1
h]
Goals accomplished! 🐙
  α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

Rat.floor a = a.num / ↑a.den.α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: ¬a.den = 1

inra.num / ↑a.den = a.num / ↑a.den α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: ¬a.den = 1

inra.num / ↑a.den = a.num / ↑a.dennext => α: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: ℚ

h✝: ¬a.den = 1

inra.num / ↑a.den = a.num / ↑a.denrfl
Goals accomplished! 🐙

protected theorem le_floor: ∀ {z : ℤ} {r : ℚ}, z ≤ Rat.floor r ↔ ↑z ≤ r
le_floor {z: ℤ
z : ℤ: Type
ℤ} : ∀ {r: ℚ
r : ℚ: Type
ℚ}, z: ℤ
z ≤ Rat.floor: ℚ → ℤ
Rat.floor r: ℚ
r ↔ (z: ℤ
z : ℚ: Type
ℚ) ≤ r: ℚ
r
  | ⟨n: ℤ
n, d: ℕ
d, h: d ≠ 0
h, c: Nat.coprime (natAbs n) d
c⟩ => by
Goals accomplished! 🐙
    α: 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 dsimp [Rat.floor_def': ∀ (a : ℚ), Rat.floor a = a.num / ↑a.den
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 ≤ 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 drw [α: 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 dnum_den': ∀ {n : ℤ} {d : ℕ} {h : d ≠ 0} {c : Nat.coprime (natAbs n) d}, mk' n d = n /. ↑d
num_den'α: 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 ≤ 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 dhave h': ?m.2020
h' := Int.ofNat_lt: ∀ {n m : ℕ}, ↑n < ↑m ↔ n < m
Int.ofNat_lt.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (Nat.pos_of_ne_zero: ∀ {n : ℕ}, n ≠ 0 → 0 < n
Nat.pos_of_ne_zero h: d ≠ 0
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 ≤ 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 dconv =>α: Type ?u.897

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

z, n: ℤ

d: ℕ

h: d ≠ 0

c: Nat.coprime (natAbs n) d

h': ↑0 < ↑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 /. ↑drhsα: 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
      α: 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 /. ↑drw [α: Type ?u.897

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

z, n: ℤ

d: ℕ

h: d ≠ 0

c: Nat.coprime (natAbs n) d

h': ↑0 < ↑d

↑z ≤ n /. ↑dcoe_int_eq_divInt: ∀ (z : ℤ), ↑z = z /. 1
coe_int_eq_divInt,α: Type ?u.897

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

z, n: ℤ

d: ℕ

h: d ≠ 0

c: Nat.coprime (natAbs n) d

h': ↑0 < ↑d

z /. 1 ≤ n /. ↑d α: Type ?u.897

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

z, n: ℤ

d: ℕ

h: d ≠ 0

c: Nat.coprime (natAbs n) d

h': ↑0 < ↑d

↑z ≤ n /. ↑dRat.le_def: ∀ {a b c d : ℤ}, 0 < b → 0 < d → (a /. b ≤ c /. d ↔ a * d ≤ c * b)
Rat.le_def zero_lt_one: ∀ {α : Type ?u.2076} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
  [inst_4 : NeZero 1], 0 < 1
zero_lt_one h': ?m.2020
h',α: Type ?u.897

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

z, n: ℤ

d: ℕ

h: d ≠ 0

c: Nat.coprime (natAbs n) d

h': ↑0 < ↑d

z * ↑d ≤ n * 1 α: Type ?u.897

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

z, n: ℤ

d: ℕ

h: d ≠ 0

c: Nat.coprime (natAbs n) d

h': ↑0 < ↑d

↑z ≤ n /. ↑dmul_one: ∀ {M : Type ?u.2702} [inst : MulOneClass M] (a : M), a * 1 = a
mul_oneα: Type ?u.897

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

z, n: ℤ

d: ℕ

h: d ≠ 0

c: Nat.coprime (natAbs n) d

h': ↑0 < ↑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 * ↑d ≤ n
    α: 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 dexact Int.le_ediv_iff_mul_le: ∀ {a b c : ℤ}, 0 < c → (a ≤ b / c ↔ a * c ≤ b)
Int.le_ediv_iff_mul_le h': ?m.2020
h'
Goals accomplished! 🐙
#align rat.le_floor Rat.le_floor: ∀ {z : ℤ} {r : ℚ}, z ≤ Rat.floor r ↔ ↑z ≤ r
Rat.le_floor

instance: FloorRing ℚ
instance : FloorRing: (α : Type ?u.3030) → [inst : LinearOrderedRing α] → Type ?u.3030
FloorRing ℚ: Type
ℚ :=
  (FloorRing.ofFloor: (α : Type ?u.3036) → [inst : LinearOrderedRing α] → (floor : α → ℤ) → GaloisConnection Int.cast floor → FloorRing α
FloorRing.ofFloor ℚ: Type
ℚ Rat.floor: ℚ → ℤ
Rat.floor) fun _: ?m.3041
_ _: ?m.3044
_ => Rat.le_floor: ∀ {z : ℤ} {r : ℚ}, z ≤ Rat.floor r ↔ ↑z ≤ r
Rat.le_floor.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm

protected theorem floor_def: ∀ {q : ℚ}, ⌊q⌋ = q.num / ↑q.den
floor_def {q: ℚ
q : ℚ: Type
ℚ} : ⌊q: ℚ
q⌋ = q: ℚ
q.num: ℚ → ℤ
num / q: ℚ
q.den: ℚ → ℕ
den := Rat.floor_def': ∀ (a : ℚ), Rat.floor a = a.num / ↑a.den
Rat.floor_def' q: ℚ
q
#align rat.floor_def Rat.floor_def: ∀ {q : ℚ}, ⌊q⌋ = q.num / ↑q.den
Rat.floor_def

theorem floor_int_div_nat_eq_div: ∀ {n : ℤ} {d : ℕ}, ⌊↑n / ↑d⌋ = n / ↑d
floor_int_div_nat_eq_div {n: ℤ
n : ℤ: Type
ℤ} {d: ℕ
d : ℕ: Type
ℕ} : ⌊(↑n: ℤ
n : ℚ: Type
ℚ) / (↑d: ℕ
d : ℚ: Type
ℚ)⌋ = n: ℤ
n / (↑d: ℕ
d : ℤ: Type
ℤ) := by
Goals accomplished! 🐙
  α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑drw [α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑dRat.floor_def: ∀ {q : ℚ}, ⌊q⌋ = q.num / ↑q.den
Rat.floor_defα: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

(↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d]α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

(↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
  α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑dobtain rfl: d = 0
rflrfl | hd: d = 0 ∨ 0 < d
 | hd: 0 < d
hd := @eq_zero_or_pos: ∀ {α : Type ?u.3669} [inst : CanonicallyOrderedAddMonoid α] {a : α}, a = 0 ∨ 0 < a
eq_zero_or_pos _: Type ?u.3669
_ _ d: ℕ
dα: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

inl(↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0
α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

hd: 0 < d

inr(↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
  α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑d·α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

inl(↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0 α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

inl(↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0
α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

hd: 0 < d

inr(↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑dsimp
Goals accomplished! 🐙
  α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑dset q: ℚ
q := (n: ℤ
n : ℚ: Type
ℚ) / d: ℕ
d with q_eq: q = ↑n / ↑d
q_eqα: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

hd: 0 < d

q:= ↑n / ↑d: ℚ

q_eq: q = ↑n / ↑d

inrq.num / ↑q.den = n / ↑d
  α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑dobtain: ∃ c, n = c * q.num ∧ ↑d = c * ↑q.den
obtain ⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩: ?m✝
⟨c: ℤ
c⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩: ?m✝
, n_eq_c_mul_num: n = c * q.num
n_eq_c_mul_num⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩: ?m✝
, d_eq_c_mul_denom: ↑d = c * ↑q.den
d_eq_c_mul_denom⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩: ?m✝
⟩ : ∃ c: ?m.5583
c, n: ℤ
n = c: ?m.5583
c * q: ℚ
q.num: ℚ → ℤ
num ∧ (d: ℕ
d : ℤ: Type
ℤ) = c: ?m.5583
c * q: ℚ
q.den: ℚ → ℕ
den := α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

hd: 0 < d

q:= ↑n / ↑d: ℚ

q_eq: q = ↑n / ↑d

inrq.num / ↑q.den = n / ↑dby
Goals accomplished! 🐙
    α: Type ?u.3373

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.denrw [α: Type ?u.3373

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.denq_eq: q = ↑n / ↑d
q_eqα: Type ?u.3373

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]α: Type ?u.3373

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
    α: Type ?u.3373

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.denexact_mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den: ∀ (n : ℤ) {d : ℤ}, d ≠ 0 → ∃ c, n = c * (↑n / ↑d).num ∧ d = c * ↑(↑n / ↑d).den
Rat.exists_eq_mul_div_num_and_eq_mul_div_den n: ℤ
n d: ℕ
d (α: Type ?u.3373

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).denby
Goals accomplished! 🐙 α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

hd: 0 < d

q:= ↑n / ↑d: ℚ

q_eq: q = ↑n / ↑d

↑d ≠ 0exact_mod_cast hd: 0 < d
hd.ne': ∀ {α : Type ?u.9155} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne'
Goals accomplished! 🐙)
Goals accomplished! 🐙
  α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑drw [α: Type ?u.3373

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

inr.intro.introq.num / ↑q.den = n / ↑dn_eq_c_mul_num: n = c * q.num
n_eq_c_mul_num,α: Type ?u.3373

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

inr.intro.introq.num / ↑q.den = c * q.num / ↑d α: Type ?u.3373

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

inr.intro.introq.num / ↑q.den = n / ↑dd_eq_c_mul_denom: ↑d = c * ↑q.den
d_eq_c_mul_denomα: Type ?u.3373

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

inr.intro.introq.num / ↑q.den = c * q.num / (c * ↑q.den)]α: Type ?u.3373

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

inr.intro.introq.num / ↑q.den = c * q.num / (c * ↑q.den)
  α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑drefine' (Int.mul_ediv_mul_of_pos: ∀ {a : ℤ} (b c : ℤ), 0 < a → a * b / (a * c) = b / c
Int.mul_ediv_mul_of_pos _: ℤ
_ _: ℤ
_ <| pos_of_mul_pos_left: ∀ {α : Type ?u.8395} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : MulPosReflectLT α],
  0 < a * b → 0 ≤ b → 0 < a
pos_of_mul_pos_left _: 0 < ?m.8397 * ?m.8398
_ <| Int.coe_nat_nonneg: ∀ (n : ℕ), 0 ≤ ↑n
Int.coe_nat_nonneg q: ℚ
q.den: ℚ → ℕ
den).symm: ∀ {α : Sort ?u.8682} {a b : α}, a = b → b = a
symmα: Type ?u.3373

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

inr.intro.intro0 < c * ↑q.den
  α: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: ℤ

d: ℕ

⌊↑n / ↑d⌋ = n / ↑drwa [α: Type ?u.3373

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

inr.intro.intro0 < c * ↑q.den← d_eq_c_mul_denom: ↑d = c * ↑q.den
d_eq_c_mul_denom,α: Type ?u.3373

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

inr.intro.intro0 < ↑d α: Type ?u.3373

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

inr.intro.intro0 < c * ↑q.denInt.coe_nat_pos: ∀ {n : ℕ}, 0 < ↑n ↔ 0 < n
Int.coe_nat_posα: Type ?u.3373

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

inr.intro.intro0 < d]α: Type ?u.3373

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

inr.intro.intro0 < d
#align rat.floor_int_div_nat_eq_div Rat.floor_int_div_nat_eq_div: ∀ {n : ℤ} {d : ℕ}, ⌊↑n / ↑d⌋ = n / ↑d
Rat.floor_int_div_nat_eq_div

@[simp, norm_cast]
theorem floor_cast: ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ⌊↑x⌋ = ⌊x⌋
floor_cast (x: ℚ
x : ℚ: Type
ℚ) : ⌊(x: ℚ
x : α: Type ?u.9242
α)⌋ = ⌊x: ℚ
x⌋ :=
  floor_eq_iff: ∀ {α : Type ?u.9347} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
floor_eq_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (by
Goals accomplished! 🐙 α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

↑⌊x⌋ ≤ ↑x ∧ ↑x < ↑⌊x⌋ + 1exact_mod_cast floor_eq_iff: ∀ {α : Type ?u.13167} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
floor_eq_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 (Eq.refl: ∀ {α : Sort ?u.13181} (a : α), a = a
Eq.refl ⌊x: ℚ
x⌋)
Goals accomplished! 🐙)
#align rat.floor_cast Rat.floor_cast: ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ⌊↑x⌋ = ⌊x⌋
Rat.floor_cast

@[simp, norm_cast]
theorem ceil_cast: ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ⌈↑x⌉ = ⌈x⌉
ceil_cast (x: ℚ
x : ℚ: Type
ℚ) : ⌈(x: ℚ
x : α: Type ?u.13509
α)⌉ = ⌈x: ℚ
x⌉ := by
Goals accomplished! 🐙
  α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌈↑x⌉ = ⌈x⌉rw [α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌈↑x⌉ = ⌈x⌉← neg_inj: ∀ {G : Type ?u.13616} [inst : InvolutiveNeg G] {a b : G}, -a = -b ↔ a = b
neg_inj,α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

-⌈↑x⌉ = -⌈x⌉ α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌈↑x⌉ = ⌈x⌉← floor_neg: ∀ {α : Type ?u.13693} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {a : α}, ⌊-a⌋ = -⌈a⌉
floor_neg,α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌊-↑x⌋ = -⌈x⌉ α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌈↑x⌉ = ⌈x⌉← floor_neg: ∀ {α : Type ?u.13740} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {a : α}, ⌊-a⌋ = -⌈a⌉
floor_neg,α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌊-↑x⌋ = ⌊-x⌋ α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌈↑x⌉ = ⌈x⌉← Rat.cast_neg: ∀ {α : Type ?u.13766} [inst : DivisionRing α] (n : ℚ), ↑(-n) = -↑n
Rat.cast_neg,α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌊↑(-x)⌋ = ⌊-x⌋ α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌈↑x⌉ = ⌈x⌉Rat.floor_cast: ∀ {α : Type ?u.13808} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ⌊↑x⌋ = ⌊x⌋
Rat.floor_castα: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

⌊-x⌋ = ⌊-x⌋]
Goals accomplished! 🐙
#align rat.ceil_cast Rat.ceil_cast: ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ⌈↑x⌉ = ⌈x⌉
Rat.ceil_cast

@[simp, norm_cast]
theorem round_cast: ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), round ↑x = round x
round_cast (x: ℚ
x : ℚ: Type
ℚ) : round: {α : Type ?u.13951} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → ℤ
round (x: ℚ
x : α: Type ?u.13924
α) = round: {α : Type ?u.14014} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → ℤ
round x: ℚ
x := by
Goals accomplished! 🐙
  -- Porting note: `simp` worked rather than `simp [H]` in mathlib3
  α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

round ↑x = round xhave H: ↑2 = 2
H : ((2: ?m.14036
2 : ℚ: Type
ℚ) : α: Type u_1
α) = (2: ?m.14088
2 : α: Type u_1
α) := Rat.cast_coe_nat: ∀ {α : Type ?u.14151} [inst : DivisionRing α] (n : ℕ), ↑↑n = ↑n
Rat.cast_coe_nat 2: ?m.14155
2α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

round ↑x = round x
  α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

round ↑x = round xhave : ((x: ℚ
x + 1: ?m.14209
1 / 2: ?m.14220
2 : ℚ: Type
ℚ) : α: Type u_1
α) = x: ℚ
x + 1: ?m.14371
1 / 2: ?m.14382
2 := α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

round ↑x = round xby
Goals accomplished! 🐙 α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

↑(x + 1 / 2) = ↑x + 1 / 2simp [H: ↑2 = 2
H]
Goals accomplished! 🐙
  α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

round ↑x = round xrw [α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

this: ↑(x + 1 / 2) = ↑x + 1 / 2

round ↑x = round xround_eq: ∀ {α : Type ?u.15202} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : α), round x = ⌊x + 1 / 2⌋
round_eq,α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

this: ↑(x + 1 / 2) = ↑x + 1 / 2

⌊↑x + 1 / 2⌋ = round x α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

this: ↑(x + 1 / 2) = ↑x + 1 / 2

round ↑x = round xround_eq: ∀ {α : Type ?u.15234} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : α), round x = ⌊x + 1 / 2⌋
round_eq,α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

this: ↑(x + 1 / 2) = ↑x + 1 / 2

⌊↑x + 1 / 2⌋ = ⌊x + 1 / 2⌋ α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

this: ↑(x + 1 / 2) = ↑x + 1 / 2

round ↑x = round x← this: ↑(x + 1 / 2) = ↑x + 1 / 2
this,α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

this: ↑(x + 1 / 2) = ↑x + 1 / 2

⌊↑(x + 1 / 2)⌋ = ⌊x + 1 / 2⌋ α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

this: ↑(x + 1 / 2) = ↑x + 1 / 2

round ↑x = round xfloor_cast: ∀ {α : Type ?u.15262} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ⌊↑x⌋ = ⌊x⌋
floor_castα: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

H: ↑2 = 2

this: ↑(x + 1 / 2) = ↑x + 1 / 2

⌊x + 1 / 2⌋ = ⌊x + 1 / 2⌋]
Goals accomplished! 🐙
#align rat.round_cast Rat.round_cast: ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), round ↑x = round x
Rat.round_cast

@[simp, norm_cast]
theorem cast_fract: ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ↑(fract x) = fract ↑x
cast_fract (x: ℚ
x : ℚ: Type
ℚ) : (↑(fract: {α : Type ?u.15416} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract x: ℚ
x) : α: Type ?u.15388
α) = fract: {α : Type ?u.15470} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract (x: ℚ
x : α: Type ?u.15388
α) := by
Goals accomplished! 🐙
  α: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: ℚ

↑(fract x) = fract ↑xsimp only [fract: {α : Type ?u.15537} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract, cast_sub: ∀ {α : Type ?u.15543} [inst : DivisionRing α] [inst_1 : CharZero α] (m n : ℚ), ↑(m - n) = ↑m - ↑n
cast_sub, cast_coe_int: ∀ {α : Type ?u.15564} [inst : DivisionRing α] (n : ℤ), ↑↑n = ↑n
cast_coe_int, floor_cast: ∀ {α : Type ?u.15575} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ⌊↑x⌋ = ⌊x⌋
floor_cast]
Goals accomplished! 🐙
#align rat.cast_fract Rat.cast_fract: ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : ℚ), ↑(fract x) = fract ↑x
Rat.cast_fract

end Rat

theorem Int.mod_nat_eq_sub_mul_floor_rat_div: ∀ {n : ℤ} {d : ℕ}, n % ↑d = n - ↑d * ⌊↑n / ↑d⌋
Int.mod_nat_eq_sub_mul_floor_rat_div {n: ℤ
n : ℤ: Type
ℤ} {d: ℕ
d : ℕ: Type
ℕ} : n: ℤ
n % d: ℕ
d = n: ℤ
n - d: ℕ
d * ⌊(n: ℤ
n : ℚ: Type
ℚ) / d: ℕ
d⌋ := by
Goals accomplished! 🐙
  n: ℤ

d: ℕ

n % ↑d = n - ↑d * ⌊↑n / ↑d⌋rw [n: ℤ

d: ℕ

n % ↑d = n - ↑d * ⌊↑n / ↑d⌋eq_sub_of_add_eq: ∀ {G : Type ?u.16411} [inst : AddGroup G] {a b c : G}, a + c = b → a = b - c
eq_sub_of_add_eq <| Int.emod_add_ediv: ∀ (a b : ℤ), a % b + b * (a / b) = a
Int.emod_add_ediv n: ℤ
n d: ℕ
d,n: ℤ

d: ℕ

n - ↑d * (n / ↑d) = n - ↑d * ⌊↑n / ↑d⌋ n: ℤ

d: ℕ

n % ↑d = n - ↑d * ⌊↑n / ↑d⌋Rat.floor_int_div_nat_eq_div: ∀ {n : ℤ} {d : ℕ}, ⌊↑n / ↑d⌋ = n / ↑d
Rat.floor_int_div_nat_eq_divn: ℤ

d: ℕ

n - ↑d * (n / ↑d) = n - ↑d * (n / ↑d)]
Goals accomplished! 🐙
#align int.mod_nat_eq_sub_mul_floor_rat_div Int.mod_nat_eq_sub_mul_floor_rat_div: ∀ {n : ℤ} {d : ℕ}, n % ↑d = n - ↑d * ⌊↑n / ↑d⌋
Int.mod_nat_eq_sub_mul_floor_rat_div

theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime: ∀ {n d : ℕ}, coprime n d → coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
Nat.coprime_sub_mul_floor_rat_div_of_coprime {n: ℕ
n d: ℕ
d : ℕ: Type
ℕ} (n_coprime_d: coprime n d
n_coprime_d : n: ℕ
n.coprime: ℕ → ℕ → Prop
coprime d: ℕ
d) :
    ((n: ℕ
n : ℤ: Type
ℤ) - d: ℕ
d * ⌊(n: ℕ
n : ℚ: Type
ℚ) / d: ℕ
d⌋).natAbs: ℤ → ℕ
natAbs.coprime: ℕ → ℕ → Prop
coprime d: ℕ
d := by
Goals accomplished! 🐙
  n, d: ℕ

n_coprime_d: coprime n d

coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) dhave : (n: ℕ
n : ℤ: Type
ℤ) % d: ℕ
d = n: ℕ
n - d: ℕ
d * ⌊(n: ℕ
n : ℚ: Type
ℚ) / d: ℕ
d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div: ∀ {n : ℤ} {d : ℕ}, n % ↑d = n - ↑d * ⌊↑n / ↑d⌋
Int.mod_nat_eq_sub_mul_floor_rat_divn, d: ℕ

n_coprime_d: coprime n d

this: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
  n, d: ℕ

n_coprime_d: coprime n d

coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) drw [n, d: ℕ

n_coprime_d: coprime n d

this: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d← this: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
thisn, d: ℕ

n_coprime_d: coprime n d

this: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

coprime (natAbs (↑n % ↑d)) d]n, d: ℕ

n_coprime_d: coprime n d

this: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

coprime (natAbs (↑n % ↑d)) d
  n, d: ℕ

n_coprime_d: coprime n d

coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) dhave : d: ℕ
d.coprime: ℕ → ℕ → Prop
coprime n: ℕ
n := n_coprime_d: coprime n d
n_coprime_d.symm: ∀ {n m : ℕ}, coprime n m → coprime m n
symmn, d: ℕ

n_coprime_d: coprime n d

this✝: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

this: coprime d n

coprime (natAbs (↑n % ↑d)) d
  n, d: ℕ

n_coprime_d: coprime n d

coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) drwa [n, d: ℕ

n_coprime_d: coprime n d

this✝: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

this: coprime d n

coprime (natAbs (↑n % ↑d)) dNat.coprime: ℕ → ℕ → Prop
Nat.coprime,n, d: ℕ

n_coprime_d: coprime n d

this✝: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

this: gcd d n = 1

coprime (natAbs (↑n % ↑d)) d n, d: ℕ

n_coprime_d: coprime n d

this✝: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

this: coprime d n

coprime (natAbs (↑n % ↑d)) dNat.gcd_rec: ∀ (m n : ℕ), gcd m n = gcd (n % m) m
Nat.gcd_recn, d: ℕ

n_coprime_d: coprime n d

this✝: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

this: gcd (n % d) d = 1

coprime (natAbs (↑n % ↑d)) d]n, d: ℕ

n_coprime_d: coprime n d

this✝: ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋

this: gcd (n % d) d = 1

coprime (natAbs (↑n % ↑d)) d at this: coprime d n
this
Goals accomplished! 🐙
#align nat.coprime_sub_mul_floor_rat_div_of_coprime Nat.coprime_sub_mul_floor_rat_div_of_coprime: ∀ {n d : ℕ}, Nat.coprime n d → Nat.coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
Nat.coprime_sub_mul_floor_rat_div_of_coprime

namespace Rat

theorem num_lt_succ_floor_mul_den: ∀ (q : ℚ), q.num < (⌊q⌋ + 1) * ↑q.den
num_lt_succ_floor_mul_den (q: ℚ
q : ℚ: Type
ℚ) : q: ℚ
q.num: ℚ → ℤ
num < (⌊q: ℚ
q⌋ + 1: ?m.17534
1) * q: ℚ
q.den: ℚ → ℕ
den := by
Goals accomplished! 🐙
  q: ℚ

q.num < (⌊q⌋ + 1) * ↑q.densuffices (q: ℚ
q.num: ℚ → ℤ
num : ℚ: Type
ℚ) < (⌊q: ℚ
q⌋ + 1: ?m.17766
1) * q: ℚ
q.den: ℚ → ℕ
den by q: ℚ

q.num < (⌊q⌋ + 1) * ↑q.denexact_mod_cast this: ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
this
Goals accomplished! 🐙
  q: ℚ

q.num < (⌊q⌋ + 1) * ↑q.densuffices (q: ℚ
q.num: ℚ → ℤ
num : ℚ: Type
ℚ) < (q: ℚ
q - fract: {α : Type ?u.21240} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q + 1: ?m.21245
1) * q: ℚ
q.den: ℚ → ℕ
den by
    q: ℚ

↑q.num < (↑⌊q⌋ + 1) * ↑q.denhave : (⌊q: ℚ
q⌋ : ℚ: Type
ℚ) = q: ℚ
q - fract: {α : Type ?u.21409} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q := eq_sub_of_add_eq: ∀ {G : Type ?u.21436} [inst : AddGroup G] {a b c : G}, a + c = b → a = b - c
eq_sub_of_add_eq <| floor_add_fract: ∀ {α : Type ?u.21465} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), ↑⌊a⌋ + fract a = a
floor_add_fract q: ℚ
qq: ℚ

this✝: ↑q.num < (q - fract q + 1) * ↑q.den

this: ↑⌊q⌋ = q - fract q

↑q.num < (↑⌊q⌋ + 1) * ↑q.den
    q: ℚ

this: ↑q.num < (q - fract q + 1) * ↑q.den

↑q.num < (↑⌊q⌋ + 1) * ↑q.denrwa [q: ℚ

this✝: ↑q.num < (q - fract q + 1) * ↑q.den

this: ↑⌊q⌋ = q - fract q

↑q.num < (↑⌊q⌋ + 1) * ↑q.denthis: ↑⌊q⌋ = q - fract q
thisq: ℚ

this✝: ↑q.num < (q - fract q + 1) * ↑q.den

this: ↑⌊q⌋ = q - fract q

↑q.num < (q - fract q + 1) * ↑q.den]q: ℚ

this✝: ↑q.num < (q - fract q + 1) * ↑q.den

this: ↑⌊q⌋ = q - fract q

↑q.num < (q - fract q + 1) * ↑q.den
  q: ℚ

q.num < (⌊q⌋ + 1) * ↑q.densuffices (q: ℚ
q.num: ℚ → ℤ
num : ℚ: Type
ℚ) < q: ℚ
q.num: ℚ → ℤ
num + (1: ?m.21659
1 - fract: {α : Type ?u.21669} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q) * q: ℚ
q.den: ℚ → ℕ
den by
    q: ℚ

↑q.num < (q - fract q + 1) * ↑q.denhave : (q: ℚ
q - fract: {α : Type ?u.21834} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q + 1: ?m.21839
1) * q: ℚ
q.den: ℚ → ℕ
den = q: ℚ
q.num: ℚ → ℤ
num + (1: ?m.21864
1 - fract: {α : Type ?u.21874} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q) * q: ℚ
q.den: ℚ → ℕ
denq: ℚ

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: ℚ

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
    q: ℚ

this: ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

↑q.num < (q - fract q + 1) * ↑q.dencalc
      (q: ℚ
q - fract: {α : Type ?u.22155} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q + 1: ?m.22160
1) * q: ℚ
q.den: ℚ → ℕ
den = (q: ℚ
q + (1: ?m.22185
1 - fract: {α : Type ?u.22195} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q)) * q: ℚ
q.den: ℚ → ℕ
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: ℚ

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.denby
Goals accomplished! 🐙 q: ℚ

this: ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

(q - fract q + 1) * ↑q.den = (q + (1 - fract q)) * ↑q.denring
Goals accomplished! 🐙
      _: ?m✝
_ = q: ℚ
q * q: ℚ
q.den: ℚ → ℕ
den + (1: ?m.22449
1 - fract: {α : Type ?u.22459} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q) * q: ℚ
q.den: ℚ → ℕ
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: ℚ

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.denby
Goals accomplished! 🐙 q: ℚ

this: ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

(q + (1 - fract q)) * ↑q.den = q * ↑q.den + (1 - fract q) * ↑q.denrw [q: ℚ

this: ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

(q + (1 - fract q)) * ↑q.den = q * ↑q.den + (1 - fract q) * ↑q.denadd_mul: ∀ {R : Type ?u.23110} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
  (a + b) * c = a * c + b * c
add_mulq: ℚ

this: ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

q * ↑q.den + (1 - fract q) * ↑q.den = q * ↑q.den + (1 - fract q) * ↑q.den]
Goals accomplished! 🐙
      _: ?m✝
_ = q: ℚ
q.num: ℚ → ℤ
num + (1: ?m.22729
1 - fract: {α : Type ?u.22739} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q) * q: ℚ
q.den: ℚ → ℕ
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: ℚ

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.denby
Goals accomplished! 🐙 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.densimp
Goals accomplished! 🐙

    q: ℚ

this: ↑q.num < ↑q.num + (1 - fract q) * ↑q.den

↑q.num < (q - fract q + 1) * ↑q.denrwa [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.denthis: (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
thisq: ℚ

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.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.num + (1 - fract q) * ↑q.den
  q: ℚ

q.num < (⌊q⌋ + 1) * ↑q.densuffices 0: ?m.23659
0 < (1: ?m.23681
1 - fract: {α : Type ?u.23691} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q) * q: ℚ
q.den: ℚ → ℕ
den by
    q: ℚ

↑q.num < ↑q.num + (1 - fract q) * ↑q.denrw [q: ℚ

this: 0 < (1 - fract q) * ↑q.den

↑q.num < ↑q.num + (1 - fract q) * ↑q.den← sub_lt_iff_lt_add': ∀ {α : Type ?u.23804} [inst : AddCommGroup α] [inst_1 : LT α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, a - b < c ↔ a < b + c
sub_lt_iff_lt_add'q: ℚ

this: 0 < (1 - fract q) * ↑q.den

↑q.num - ↑q.num < (1 - fract q) * ↑q.den]q: ℚ

this: 0 < (1 - fract q) * ↑q.den

↑q.num - ↑q.num < (1 - fract q) * ↑q.den
    q: ℚ

this: 0 < (1 - fract q) * ↑q.den

↑q.num < ↑q.num + (1 - fract q) * ↑q.densimpa
Goals accomplished! 🐙
  q: ℚ

q.num < (⌊q⌋ + 1) * ↑q.denhave : 0: ?m.27487
0 < 1: ?m.27506
1 - fract: {α : Type ?u.27516} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q := q: ℚ

0 < (1 - fract q) * ↑q.denby
Goals accomplished! 🐙
    q: ℚ

0 < 1 - fract qhave : fract: {α : Type ?u.27560} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q < 1: ?m.27565
1 := fract_lt_one: ∀ {α : Type ?u.27582} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), fract a < 1
fract_lt_one q: ℚ
qq: ℚ

this: fract q < 1

0 < 1 - fract q
    q: ℚ

0 < 1 - fract qhave : 0: ?m.27596
0 + fract: {α : Type ?u.27606} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q < 1: ?m.27616
1 := q: ℚ

this: fract q < 1

0 < 1 - fract qby
Goals accomplished! 🐙 q: ℚ

this: fract q < 1

0 + fract q < 1simp [this: fract q < 1
this]
Goals accomplished! 🐙
    q: ℚ

0 < 1 - fract qrwa [q: ℚ

this✝: fract q < 1

this: 0 + fract q < 1

0 < 1 - fract qlt_sub_iff_add_lt: ∀ {α : Type ?u.27748} [inst : AddGroup α] [inst_1 : LT α]
  [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
  a < c - b ↔ a + b < c
lt_sub_iff_add_ltq: ℚ

this✝: fract q < 1

this: 0 + fract q < 1

0 + fract q < 1]q: ℚ

this✝: fract q < 1

this: 0 + fract q < 1

0 + fract q < 1
  q: ℚ

q.num < (⌊q⌋ + 1) * ↑q.denexact mul_pos: ∀ {α : Type ?u.27893} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α],
  0 < a → 0 < b → 0 < a * b
mul_pos this: 0 < 1 - fract q
this (q: ℚ

this: 0 < 1 - fract q

0 < (1 - fract q) * ↑q.denby
Goals accomplished! 🐙 q: ℚ

this: 0 < 1 - fract q

0 < ↑q.denexact_mod_cast q: ℚ
q.pos: ∀ (a : ℚ), 0 < a.den
pos
Goals accomplished! 🐙)
Goals accomplished! 🐙
#align rat.num_lt_succ_floor_mul_denom Rat.num_lt_succ_floor_mul_den: ∀ (q : ℚ), q.num < (⌊q⌋ + 1) * ↑q.den
Rat.num_lt_succ_floor_mul_den

theorem fract_inv_num_lt_num_of_pos: ∀ {q : ℚ}, 0 < q → (fract q⁻¹).num < q.num
fract_inv_num_lt_num_of_pos {q: ℚ
q : ℚ: Type
ℚ} (q_pos: 0 < q
q_pos : 0: ?m.28058
0 < q: ℚ
q) : (fract: {α : Type ?u.28094} → [inst : LinearOrderedRing α] → [inst : FloorRing α] → α → α
fract q: ℚ
q⁻¹).num: ℚ → ℤ
num < q: ℚ
q.num: ℚ → ℤ
num := by
Goals accomplished! 🐙
  -- we know that the numerator must be positive
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numhave q_num_pos: 0 < q.num
q_num_pos : 0: ?m.28163
0 < q: ℚ
q.num: ℚ → ℤ
num := Rat.num_pos_iff_pos: ∀ {a : ℚ}, 0 < a.num ↔ 0 < a
Rat.num_pos_iff_pos.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr q_pos: 0 < q
q_posq: ℚ

q_pos: 0 < q

q_num_pos: 0 < q.num

(fract q⁻¹).num < q.num
  -- we will work with the absolute value of the numerator, which is equal to the numerator
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numhave q_num_abs_eq_q_num: ↑(natAbs q.num) = q.num
q_num_abs_eq_q_num : (q: ℚ
q.num: ℚ → ℤ
num.natAbs: ℤ → ℕ
natAbs : ℤ: Type
ℤ) = q: ℚ
q.num: ℚ → ℤ
num := Int.natAbs_of_nonneg: ∀ {a : ℤ}, 0 ≤ a → ↑(natAbs a) = a
Int.natAbs_of_nonneg q_num_pos: 0 < q.num
q_num_pos.le: ∀ {α : Type ?u.28256} [inst : Preorder α] {a b : α}, a < b → a ≤ b
leq: ℚ

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
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numset q_inv: ℚ
q_inv := (q: ℚ
q.den: ℚ → ℕ
den : ℚ: Type
ℚ) / q: ℚ
q.num: ℚ → ℤ
num with q_inv_def: q_inv = ↑q.den / ↑q.num
q_inv_defq: ℚ

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
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numhave q_inv_eq: q⁻¹ = q_inv
q_inv_eq : q: ℚ
q⁻¹ = q_inv: ℚ
q_inv := Rat.inv_def'': ∀ {q : ℚ}, q⁻¹ = ↑q.den / ↑q.num
Rat.inv_def''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
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numsuffices (q_inv: ℚ
q_inv - ⌊q_inv: ℚ
q_inv⌋).num: ℚ → ℤ
num < q: ℚ
q.num: ℚ → ℤ
num by 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.numrwa [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.numq_inv_eq: q⁻¹ = q_inv
q_inv_eqq: ℚ

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_inv).num < q.num]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_inv).num < q.num
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numsuffices ((q: ℚ
q.den: ℚ → ℕ
den - q: ℚ
q.num: ℚ → ℤ
num * ⌊q_inv: ℚ
q_inv⌋ : ℚ: Type
ℚ) / q: ℚ
q.num: ℚ → ℤ
num).num: ℚ → ℤ
num < q: ℚ
q.num: ℚ → ℤ
num by
    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.numfield_simp [this: ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
this, ne_of_gt: ∀ {α : Type ?u.29520} [inst : Preorder α] {a b : α}, b < a → a ≠ b
ne_of_gt q_num_pos: 0 < q.num
q_num_pos]
Goals accomplished! 🐙
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numsuffices (q: ℚ
q.den: ℚ → ℕ
den : ℤ: Type
ℤ) - q: ℚ
q.num: ℚ → ℤ
num * ⌊q_inv: ℚ
q_inv⌋ < q: ℚ
q.num: ℚ → ℤ
num by
    -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
    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.numhave : ((q: ℚ
q.den: ℚ → ℕ
den - q: ℚ
q.num: ℚ → ℤ
num * ⌊q_inv: ℚ
q_inv⌋ : ℚ: Type
ℚ) / q: ℚ
q.num: ℚ → ℤ
num).num: ℚ → ℤ
num = q: ℚ
q.den: ℚ → ℕ
den - q: ℚ
q.num: ℚ → ℤ
num * ⌊q_inv: ℚ
q_inv⌋ := 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.numby
Goals accomplished! 🐙
      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⌋suffices ((q: ℚ
q.den: ℚ → ℕ
den : ℤ: Type
ℤ) - q: ℚ
q.num: ℚ → ℤ
num * ⌊q_inv: ℚ
q_inv⌋).natAbs: ℤ → ℕ
natAbs.coprime: ℕ → ℕ → Prop
coprime q: ℚ
q.num: ℚ → ℤ
num.natAbs: ℤ → ℕ
natAbs by
        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⌋exact_mod_cast Rat.num_div_eq_of_coprime: ∀ {a b : ℤ}, 0 < b → Nat.coprime (natAbs a) (natAbs b) → (↑a / ↑b).num = a
Rat.num_div_eq_of_coprime q_num_pos: 0 < q.num
q_num_pos this: Nat.coprime (natAbs (↑q.den - q.num * ⌊q_inv⌋)) (natAbs q.num)
this
Goals accomplished! 🐙
      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⌋have tmp: ?m.31139
tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime: ∀ {n d : ℕ}, Nat.coprime n d → Nat.coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
Nat.coprime_sub_mul_floor_rat_div_of_coprime q: ℚ
q.reduced: ∀ (self : ℚ), Nat.coprime (natAbs self.num) self.den
reduced.symm: ∀ {n m : ℕ}, Nat.coprime n m → Nat.coprime m n
symmq: ℚ

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)
      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⌋simpa only [Nat.cast_natAbs: ∀ {α : Type ?u.31162} [inst : AddGroupWithOne α] (n : ℤ), ↑(natAbs n) = ↑(abs n)
Nat.cast_natAbs, abs_of_nonneg: ∀ {α : Type ?u.31175} [inst : AddGroup α] [inst_1 : LinearOrder α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 ≤ a → abs a = a
abs_of_nonneg q_num_pos: 0 < q.num
q_num_pos.le: ∀ {α : Type ?u.31181} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le] using tmp: ?m.31139
tmp
Goals accomplished! 🐙
    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.numrwa [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.numthis: ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
thisq: ℚ

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]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
  -- to show the claim, start with the following inequality
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numhave q_inv_num_denom_ineq: q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
q_inv_num_denom_ineq : q: ℚ
q⁻¹.num: ℚ → ℤ
num - ⌊q: ℚ
q⁻¹⌋ * q: ℚ
q⁻¹.den: ℚ → ℕ
den < q: ℚ
q⁻¹.den: ℚ → ℕ
den := 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.numby
Goals accomplished! 🐙
    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⁻¹.denhave : q: ℚ
q⁻¹.num: ℚ → ℤ
num < (⌊q: ℚ
q⁻¹⌋ + 1: ?m.31708
1) * q: ℚ
q⁻¹.den: ℚ → ℕ
den := Rat.num_lt_succ_floor_mul_den: ∀ (q : ℚ), q.num < (⌊q⌋ + 1) * ↑q.den
Rat.num_lt_succ_floor_mul_den q: ℚ
q⁻¹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
    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⁻¹.denhave : q: ℚ
q⁻¹.num: ℚ → ℤ
num < ⌊q: ℚ
q⁻¹⌋ * q: ℚ
q⁻¹.den: ℚ → ℕ
den + q: ℚ
q⁻¹.den: ℚ → ℕ
den := 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⁻¹.denby
Goals accomplished! 🐙 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⁻¹.denrwa [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⁻¹.denright_distrib: ∀ {R : Type ?u.32029} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
  (a + b) * c = a * c + b * c
right_distrib,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⁻¹⌋ * ↑q⁻¹.den + 1 * ↑q⁻¹.den

q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den 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⁻¹.denone_mul: ∀ {M : Type ?u.32237} [inst : MulOneClass M] (a : M), 1 * a = a
one_mulq: ℚ

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⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den

q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den]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⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den

q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den at this: q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
this
Goals accomplished! 🐙
    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⁻¹.denrwa [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← sub_lt_iff_lt_add': ∀ {α : Type ?u.32324} [inst : AddCommGroup α] [inst_1 : LT α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, a - b < c ↔ a < b + c
sub_lt_iff_lt_add'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]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 at this: q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
this
Goals accomplished! 🐙
  -- use that `q.num` and `q.den` are coprime to show that q_inv is the unreduced reciprocal
  -- of `q`
  q: ℚ

q_pos: 0 < q

(fract q⁻¹).num < q.numhave : q_inv: ℚ
q_inv.num: ℚ → ℤ
num = q: ℚ
q.den: ℚ → ℕ
den ∧ q_inv: ℚ
q_inv.den: ℚ → ℕ
den = q: ℚ
q.num: ℚ → ℤ
num.natAbs: ℤ → ℕ
natAbs := 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.numby
Goals accomplished! 🐙
    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.numhave coprime_q_denom_q_num: Nat.coprime q.den (natAbs q.num)
coprime_q_denom_q_num : q: ℚ
q.den: ℚ → ℕ
den.coprime: ℕ → ℕ → Prop
coprime q: ℚ
q.num: ℚ → ℤ
num.natAbs: ℤ → ℕ
natAbs := q: ℚ
q.reduced: ∀ (self : ℚ), Nat.coprime (natAbs self.num) self.den
reduced.symm: ∀ {n m : ℕ}, Nat.coprime n m → Nat.coprime m n
symmq: ℚ

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
    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.numhave : Int.natAbs: ℤ → ℕ
Int.natAbs q: ℚ
q.den: ℚ → ℕ
den = q: ℚ
q.den: ℚ → ℕ
den := 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.numby
Goals accomplished! 🐙 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.densimp
Goals accomplished! 🐙
    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.numrw [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← this: natAbs ↑q.den = q.den
thisq: ℚ

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]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 at coprime_q_denom_q_num: Nat.coprime q.den (natAbs q.num)
coprime_q_denom_q_numq: ℚ

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
    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.numrw [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.numq_inv_def: q_inv = ↑q.den / ↑q.num
q_inv_defq: ℚ

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]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
    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.numconstructorq: ℚ

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

left(↑q.den / ↑q.num).num = ↑q.den
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

right(↑q.den / ↑q.num).den = natAbs q.num
    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·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

left(↑q.den / ↑q.num).num = ↑q.den 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

left(↑q.den / ↑q.num).num = ↑q.den
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

right(↑q.den / ↑q.num).den = natAbs q.numexact_mod_cast Rat.num_div_eq_of_coprime: ∀ {a b : ℤ}, 0 < b → Nat.coprime (natAbs a) (natAbs b) → (↑a / ↑b).num = a
Rat.num_div_eq_of_coprime q_num_pos: 0 < q.num
q_num_pos coprime_q_denom_q_num: Nat.coprime (natAbs ↑q.den) (natAbs q.num)
coprime_q_denom_q_num
Goals accomplished! 🐙
    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