Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
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 :
β„š: Type
β„š
) : a.
floor: β„š β†’ β„€
floor
= a.
num: β„š β†’ β„€
num
/ a.
den: β„š β†’ β„•
den
:=

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: β„š


Rat.floor a = 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: β„š


(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.den
Ξ±: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: β„š

h✝: a.den = 1


inl
a.num = a.num / ↑a.den
Ξ±: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: β„š

h✝: ¬a.den = 1


inr
a.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


inl
a.num = a.num / ↑a.den
Ξ±: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: β„š

h✝: a.den = 1


inl
a.num = a.num / ↑a.den
Ξ±: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: β„š

h✝: ¬a.den = 1


inr
a.num / ↑a.den = a.num / ↑a.den
Ξ±: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: β„š

h✝: a.den = 1


inl
a.num = a.num / ↑a.den

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


inr
a.num / ↑a.den = a.num / ↑a.den
Ξ±: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: β„š

h✝: ¬a.den = 1


inr
a.num / ↑a.den = a.num / ↑a.den
Ξ±: Type ?u.26

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

a: β„š

h✝: ¬a.den = 1


inr
a.num / ↑a.den = a.num / ↑a.den

Goals accomplished! πŸ™
protected theorem
le_floor: βˆ€ {z : β„€} {r : β„š}, z ≀ Rat.floor r ↔ ↑z ≀ r
le_floor
{z :
β„€: Type
β„€
} : βˆ€ {r :
β„š: Type
β„š
}, z ≀
Rat.floor: β„š β†’ β„€
Rat.floor
r ↔ (z :
β„š: Type
β„š
) ≀ r | ⟨n, d,
h: d β‰  0
h
, c⟩ =>

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 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
Ξ±: 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
Ξ±: 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 ≀ 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 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 /. ↑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
Ξ±: 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 /. ↑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
Ξ±: 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

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 /. 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 /. ↑d
Ξ±: 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 /. ↑d
Ξ±: 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 d

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 :
β„š: Type
β„š
} : ⌊qβŒ‹ = q.
num: β„š β†’ β„€
num
/ q.
den: β„š β†’ β„•
den
:=
Rat.floor_def': βˆ€ (a : β„š), Rat.floor a = a.num / ↑a.den
Rat.floor_def'
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 :
β„€: Type
β„€
} {d :
β„•: Type
β„•
} : ⌊(↑n :
β„š: Type
β„š
) / (↑d :
β„š: Type
β„š
)βŒ‹ = n / (↑d :
β„€: Type
β„€
) :=

Goals accomplished! πŸ™
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•


βŒŠβ†‘n / ↑dβŒ‹ = n / ↑d
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•


βŒŠβ†‘n / ↑dβŒ‹ = 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).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: β„€

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 / ↑d

Goals accomplished! πŸ™
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•


βŒŠβ†‘n / ↑dβŒ‹ = n / ↑d
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•

hd: 0 < d

q:= ↑n / ↑d: β„š

q_eq: q = ↑n / ↑d


inr
q.num / ↑q.den = n / ↑d
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•


βŒŠβ†‘n / ↑dβŒ‹ = n / ↑d
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•

hd: 0 < d

q:= ↑n / ↑d: β„š

q_eq: q = ↑n / ↑d


inr
q.num / ↑q.den = n / ↑d

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.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.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 * (↑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.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

Goals accomplished! πŸ™
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•

hd: 0 < d

q:= ↑n / ↑d: β„š

q_eq: q = ↑n / ↑d


↑d β‰  0

Goals accomplished! πŸ™

Goals accomplished! πŸ™
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•


βŒŠβ†‘n / ↑dβŒ‹ = n / ↑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.intro
q.num / ↑q.den = n / ↑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.intro
q.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.intro
q.num / ↑q.den = n / ↑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.intro
q.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.intro
q.num / ↑q.den = c * q.num / (c * ↑q.den)
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•


βŒŠβ†‘n / ↑dβŒ‹ = n / ↑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.intro
0 < c * ↑q.den
Ξ±: Type ?u.3373

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

n: β„€

d: β„•


βŒŠβ†‘n / ↑dβŒ‹ = n / ↑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.intro
0 < 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.intro
0 < ↑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.intro
0 < 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.intro
0 < 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.intro
0 < 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 :
β„š: Type
β„š
) : ⌊(x :
Ξ±: Type ?u.9242
Ξ±
)βŒ‹ = ⌊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
(

Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


β†‘βŒŠxβŒ‹ ≀ ↑x ∧ ↑x < β†‘βŒŠxβŒ‹ + 1

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 :
β„š: Type
β„š
) : ⌈(x :
Ξ±: Type ?u.13509
Ξ±
)βŒ‰ = ⌈xβŒ‰ :=

Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

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 :
β„š: Type
β„š
) :
round: {Ξ± : Type ?u.13951} β†’ [inst : LinearOrderedRing Ξ±] β†’ [inst : FloorRing Ξ±] β†’ Ξ± β†’ β„€
round
(x :
Ξ±: Type ?u.13924
Ξ±
) =
round: {Ξ± : Type ?u.14014} β†’ [inst : LinearOrderedRing Ξ±] β†’ [inst : FloorRing Ξ±] β†’ Ξ± β†’ β„€
round
x :=

Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


round ↑x = round x
Ξ±: 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 x
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š

H: ↑2 = 2


round ↑x = round x

Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š

H: ↑2 = 2


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

Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


round ↑x = round x
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š

H: ↑2 = 2

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


round ↑x = round x
Ξ±: 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 x
Ξ±: 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
Ξ±: 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
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š

H: ↑2 = 2

this: ↑(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 :
β„š: Type
β„š
) : (↑(
fract: {Ξ± : Type ?u.15416} β†’ [inst : LinearOrderedRing Ξ±] β†’ [inst : FloorRing Ξ±] β†’ Ξ± β†’ Ξ±
fract
x) :
Ξ±: Type ?u.15388
Ξ±
) =
fract: {Ξ± : Type ?u.15470} β†’ [inst : LinearOrderedRing Ξ±] β†’ [inst : FloorRing Ξ±] β†’ Ξ± β†’ Ξ±
fract
(x :
Ξ±: Type ?u.15388
Ξ±
) :=

Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝¹: LinearOrderedField α

inst✝: FloorRing α

x: β„š


↑(fract x) = fract ↑x

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 :
β„€: Type
β„€
} {d :
β„•: Type
β„•
} : n % d = n - d * ⌊(n :
β„š: Type
β„š
) / dβŒ‹ :=

Goals accomplished! πŸ™

n % ↑d = n - ↑d * βŒŠβ†‘n / ↑dβŒ‹

n % ↑d = n - ↑d * βŒŠβ†‘n / ↑dβŒ‹

n - ↑d * (n / ↑d) = n - ↑d * βŒŠβ†‘n / ↑dβŒ‹

n % ↑d = n - ↑d * βŒŠβ†‘n / ↑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 d :
β„•: Type
β„•
} (
n_coprime_d: coprime n d
n_coprime_d
: n.
coprime: β„• β†’ β„• β†’ Prop
coprime
d) : ((n :
β„€: Type
β„€
) - d * ⌊(n :
β„š: Type
β„š
) / dβŒ‹).
natAbs: β„€ β†’ β„•
natAbs
.
coprime: β„• β†’ β„• β†’ Prop
coprime
d :=

Goals accomplished! πŸ™
n, d: β„•

n_coprime_d: coprime n d


coprime (natAbs (↑n - ↑d * βŒŠβ†‘n / ↑dβŒ‹)) d
n, 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βŒ‹)) d
n, 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

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βŒ‹)) d
n, 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βŒ‹)) d
n, 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

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)) 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
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

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 :
β„š: Type
β„š
) : q.
num: β„š β†’ β„€
num
< (⌊qβŒ‹ +
1: ?m.17534
1
) * q.
den: β„š β†’ β„•
den
:=

Goals accomplished! πŸ™

q.num < (⌊qβŒ‹ + 1) * ↑q.den

q.num < (⌊qβŒ‹ + 1) * ↑q.den

Goals accomplished! πŸ™

q.num < (⌊qβŒ‹ + 1) * ↑q.den

↑q.num < (β†‘βŒŠqβŒ‹ + 1) * ↑q.den
q: β„š

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.den
q: β„š

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

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.num < (⌊qβŒ‹ + 1) * ↑q.den

↑q.num < (q - fract q + 1) * ↑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: β„š

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.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.den

Goals accomplished! πŸ™
q: β„š

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


(q - fract q + 1) * ↑q.den = (q + (1 - fract q)) * ↑q.den

Goals accomplished! πŸ™
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.den

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.den
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
q: β„š

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! πŸ™
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.den

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.den

Goals accomplished! πŸ™
q: β„š

this: ↑q.num < ↑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

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

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.num < (⌊qβŒ‹ + 1) * ↑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.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.den

Goals accomplished! πŸ™

q.num < (⌊qβŒ‹ + 1) * ↑q.den

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

Goals accomplished! πŸ™

0 < 1 - fract q
q: β„š

this: fract q < 1


0 < 1 - fract q

0 < 1 - fract q
q: β„š

this: fract q < 1


0 < 1 - fract q

Goals accomplished! πŸ™
q: β„š

this: fract q < 1


0 + fract q < 1

Goals accomplished! πŸ™

0 < 1 - fract q
q: β„š

this✝: fract q < 1

this: 0 + fract q < 1


0 < 1 - fract q
q: β„š

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.num < (⌊qβŒ‹ + 1) * ↑q.den
q: β„š

this: 0 < 1 - fract q


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

Goals accomplished! πŸ™
q: β„š

this: 0 < 1 - fract q


0 < ↑q.den

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 :
β„š: Type
β„š
} (
q_pos: 0 < q
q_pos
:
0: ?m.28058
0
< q) : (
fract: {Ξ± : Type ?u.28094} β†’ [inst : LinearOrderedRing Ξ±] β†’ [inst : FloorRing Ξ±] β†’ Ξ± β†’ Ξ±
fract
q⁻¹).
num: β„š β†’ β„€
num
< q.
num: β„š β†’ β„€
num
:=

Goals accomplished! πŸ™
q: β„š

q_pos: 0 < q


(fract q⁻¹).num < q.num
q: β„š

q_pos: 0 < q

q_num_pos: 0 < q.num


(fract q⁻¹).num < q.num
q: β„š

q_pos: 0 < q


(fract q⁻¹).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


(fract q⁻¹).num < q.num
q: β„š

q_pos: 0 < q


(fract q⁻¹).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


(fract q⁻¹).num < q.num
q: β„š

q_pos: 0 < q


(fract q⁻¹).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


(fract q⁻¹).num < q.num
q: β„š

q_pos: 0 < q


(fract q⁻¹).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


(fract q⁻¹).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⁻¹).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

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.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 - β†‘βŒŠq_invβŒ‹).num < q.num

Goals accomplished! πŸ™
q: β„š

q_pos: 0 < q


(fract q⁻¹).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


((↑q.den - ↑q.num * β†‘βŒŠq_invβŒ‹) / ↑q.num).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.den - q.num * ⌊q_invβŒ‹ < q.num


((↑q.den - ↑q.num * β†‘βŒŠq_invβŒ‹) / ↑q.num).num < 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

this: ↑q.den - q.num * ⌊q_invβŒ‹ < q.num


((↑q.den - ↑q.num * β†‘βŒŠq_invβŒ‹) / ↑q.num).num = ↑q.den - q.num * ⌊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.den - q.num * ⌊q_invβŒ‹

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βŒ‹
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)
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βŒ‹

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.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).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.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
q: β„š

q_pos: 0 < q


(fract q⁻¹).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


↑q.den - q.num * ⌊q_invβŒ‹ < 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: β„š

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: β„š

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: β„š

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



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: β„š

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: β„š

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: β„š

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: β„š

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: β„š

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



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: β„š

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: β„š

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: β„š

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



Goals accomplished! πŸ™
q: β„š

q_pos: 0 < q


(fract q⁻¹).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

q_inv_num_denom_ineq: q⁻¹.num - ⌊qβ»ΒΉβŒ‹ * ↑q⁻¹.den < ↑q⁻¹.den


↑q.den - q.num * ⌊q_invβŒ‹ < 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⁻¹.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 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.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 q.den (natAbs q.num)


q_inv.num = ↑q.den ∧ q_inv.den = natAbs 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⁻¹.den < ↑q⁻¹.den

coprime_q_denom_q_num: Nat.coprime q.den (natAbs q.num)


natAbs ↑q.den = q.den

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.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 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
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
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
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


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.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.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


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.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