case inl
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
⊢ fract (↑m / ↑0) = ↑(m % ↑0) / ↑0

case inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : n > 0
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
rcases n.eq_zero_or_pos with (rfl | hn)
case hn
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : n > 0
⊢ 0 < ↑n

case inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
case inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : n > 0
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
replace hn : 0 < (n : k)
case inr.intro.inl
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑↑m₀ / ↑n) = ↑(↑m₀ % ↑n) / ↑n

case inr.intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
case inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg
case inr.intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
case inr.intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
let q := ⌈↑m₀ / (n : k)⌉
case inr.intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
case inr.intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
let m₁ := q * ↑n - (↑m₀ : ℤ)
case inr.intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
case inr.intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
have hm₁ : 0 ≤ m₁ := by
  simpa [← @cast_le k, ← div_le_iff hn] using FloorRing.gc_ceil_coe.le_u_l _
case inr.intro.inr.calc_1
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (-↑m₀ / ↑n) = fract (↑m₁ / ↑n)

case inr.intro.inr.calc_2
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ ↑(m₁ % ↑n) / ↑n = ↑(-↑m₀ % ↑n) / ↑n
case inr.intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
calc
  fract ((Int.cast (-(m₀ : ℤ)) : k) / (n : k))
    = fract (-(m₀ : k) / n) := by rw [cast_neg, cast_ofNat]
  _ = fract ((m₁ : k) / n) := ?_
  _ = Int.cast (m₁ % (n : ℤ)) / Nat.cast n := this hm₁
  _ = Int.cast (-(↑m₀ : ℤ) % ↑n) / Nat.cast n := ?_
no goals
case inl
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
⊢ fract (↑m / ↑0) = ↑(m % ↑0) / ↑0
simp
no goals
case hn
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : n > 0
⊢ 0 < ↑n
norm_cast
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
l : ℤ
hl : 0 ≤ l
⊢ fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
⊢ ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
intros l hl
case intro.inl
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ ↑l₀
⊢ fract (↑↑l₀ / ↑n) = ↑(↑l₀ % ↑n) / ↑n

case intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ -↑l₀
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
l : ℤ
hl : 0 ≤ l
⊢ fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
no goals
case intro.inl
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ ↑l₀
⊢ fract (↑↑l₀ / ↑n) = ↑(↑l₀ % ↑n) / ↑n
rw [cast_ofNat, ← coe_nat_mod, cast_ofNat, fract_div_natCast_eq_div_natCast_mod]
case intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : l₀ = 0
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n
case intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ -↑l₀
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n
rw [Right.nonneg_neg_iff, coe_nat_nonpos_iff] at hl
no goals
case intro.inr
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : l₀ = 0
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n
simp [hl, zero_mod]
no goals
case inr.intro.inl
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑↑m₀ / ↑n) = ↑(↑m₀ % ↑n) / ↑n
exact this (ofNat_nonneg m₀)
no goals
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ 0 ≤ m₁
simpa [← @cast_le k, ← div_le_iff hn] using FloorRing.gc_ceil_coe.le_u_l _
no goals
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = fract (-↑m₀ / ↑n)
rw [cast_neg, cast_ofNat]
case inr.intro.inr.calc_1
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n - ↑m₀) / ↑n) = fract (↑m₁ / ↑n)
case inr.intro.inr.calc_1
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (-↑m₀ / ↑n) = fract (↑m₁ / ↑n)
rw [← fract_int_add q, ← mul_div_cancel (q : k) (ne_of_gt hn), ← add_div, ← sub_eq_add_neg]
no goals
case inr.intro.inr.calc_1
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n - ↑m₀) / ↑n) = fract (↑m₁ / ↑n)
simp
case inr.intro.inr.calc_2.e_a.e_a
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ m₁ % ↑n = -↑m₀ % ↑n
case inr.intro.inr.calc_2
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ ↑(m₁ % ↑n) / ↑n = ↑(-↑m₀ % ↑n) / ↑n
congr 2
case inr.intro.inr.calc_2.e_a.e_a
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ (q * ↑n - ↑m₀) % ↑n = -↑m₀ % ↑n
case inr.intro.inr.calc_2.e_a.e_a
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ m₁ % ↑n = -↑m₀ % ↑n
change (q * ↑n - (↑m₀ : ℤ)) % ↑n = _
no goals
case inr.intro.inr.calc_2.e_a.e_a
F : Type ?u.196930
α : Type ?u.196933
β : Type ?u.196936
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ (q * ↑n - ↑m₀) % ↑n = -↑m₀ % ↑n
rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self]