case inl
F : Type ?u.288255
α : Type u_1
β : Type ?u.288261
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m : ℕ
⊢ abs (↑m / ↑0 - ↑(round (↑m / ↑0))) = ↑(min (m % 0) (0 - m % 0)) / ↑0

case inr
F : Type ?u.288255
α : Type u_1
β : Type ?u.288261
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ abs (↑m / ↑n - ↑(round (↑m / ↑n))) = ↑(min (m % n) (n - m % n)) / ↑n
F : Type ?u.288255
α : Type u_1
β : Type ?u.288261
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
⊢ abs (↑m / ↑n - ↑(round (↑m / ↑n))) = ↑(min (m % n) (n - m % n)) / ↑n
rcases n.eq_zero_or_pos with (rfl | hn)
case inr
F : Type ?u.288255
α : Type u_1
β : Type ?u.288261
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ abs (↑m / ↑n - ↑(round (↑m / ↑n))) = ↑(min (m % n) (n - m % n)) / ↑n
case inr
F : Type ?u.288255
α : Type u_1
β : Type ?u.288261
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ abs (↑m / ↑n - ↑(round (↑m / ↑n))) = ↑(min (m % n) (n - m % n)) / ↑n
have hn' : 0 < (n : α) := by
  norm_cast
no goals
case inr
F : Type ?u.288255
α : Type u_1
β : Type ?u.288261
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ abs (↑m / ↑n - ↑(round (↑m / ↑n))) = ↑(min (m % n) (n - m % n)) / ↑n
rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
  fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
no goals
case inl
F : Type ?u.288255
α : Type u_1
β : Type ?u.288261
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m : ℕ
⊢ abs (↑m / ↑0 - ↑(round (↑m / ↑0))) = ↑(min (m % 0) (0 - m % 0)) / ↑0
simp
no goals
F : Type ?u.288255
α : Type u_1
β : Type ?u.288261
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ 0 < ↑n
norm_cast