case inl
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
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.187926
α : Type ?u.187929
β : Type ?u.187932
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.187926
α : Type ?u.187929
β : Type ?u.187932
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 inr
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ fract (↑m / ↑n) = ↑(m % n) / ↑n
case inr
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
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
have hn' : 0 < (n : k) := by
  norm_cast
case inr.refine_1
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ 0 ≤ ↑(m % n) / ↑n

case inr.refine_2
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑(m % n) / ↑n < 1

case inr.refine_3
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)
case inr
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ fract (↑m / ↑n) = ↑(m % n) / ↑n
refine fract_eq_iff.mpr ⟨?_, ?_, m / n, ?_⟩
no goals
case inl
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
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
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
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
no goals
case inr.refine_1
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ 0 ≤ ↑(m % n) / ↑n
positivity
no goals
case inr.refine_2
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑(m % n) / ↑n < 1
simpa only [div_lt_one hn', Nat.cast_lt] using m.mod_lt hn
case inr.refine_3
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑n * ↑(↑m / ↑n)
case inr.refine_3
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)
rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne', mul_div_cancel' _ hn'.ne', mul_add,
  mul_div_cancel' _ hn'.ne']
case inr.refine_3
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑(n * (m / n))
case inr.refine_3
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑n * ↑(↑m / ↑n)
norm_cast
no goals
case inr.refine_3
F : Type ?u.187926
α : Type ?u.187929
β : Type ?u.187932
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑(m % n) + ↑(n * (m / n))
rw [← Nat.cast_add, Nat.mod_add_div m n]