case zero
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ ∃ z, fract a * ↑Nat.zero - fract (a * ↑Nat.zero) = ↑z

case succ
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
c : ℕ
hc : ∃ z, fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(Nat.succ c) - fract (a * ↑(Nat.succ c)) = ↑z
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
b : ℕ
⊢ ∃ z, fract a * ↑b - fract (a * ↑b) = ↑z
induction' b with c hc
case zero
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ fract a * ↑Nat.zero - fract (a * ↑Nat.zero) = ↑0
case zero
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ ∃ z, fract a * ↑Nat.zero - fract (a * ↑Nat.zero) = ↑z
use 0
no goals
case zero
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
⊢ fract a * ↑Nat.zero - fract (a * ↑Nat.zero) = ↑0
simp
case succ.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(Nat.succ c) - fract (a * ↑(Nat.succ c)) = ↑z
case succ
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a✝ a : α
c : ℕ
hc : ∃ z, fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(Nat.succ c) - fract (a * ↑(Nat.succ c)) = ↑z
rcases hc with ⟨z, hz⟩
case succ.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z
case succ.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(Nat.succ c) - fract (a * ↑(Nat.succ c)) = ↑z
rw [Nat.succ_eq_add_one, Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
case succ.intro.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z
case succ.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z
rcases fract_add (a * c) a with ⟨y, hy⟩
case succ.intro.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = ↑(z - y)
case succ.intro.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z
use z - y
case succ.intro.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) =
    fract a * ↑c - fract (a * ↑c) - (fract (a * ↑c + a) - fract (a * ↑c) - fract a)
case succ.intro.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = ↑(z - y)
rw [Int.cast_sub, ← hz, ← hy]
no goals
case succ.intro.intro
F : Type ?u.175899
α : Type u_1
β : Type ?u.175905
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z✝ : ℤ
a✝ a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) =
    fract a * ↑c - fract (a * ↑c) - (fract (a * ↑c + a) - fract (a * ↑c) - fract a)
abel