case h.e'_3.h.e'_5
F : Type ?u.97534
α : Type u_1
β : Type ?u.97540
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
m n : ℕ
⊢ m = ⌊↑m⌋₊
F : Type ?u.97534
α : Type u_1
β : Type ?u.97540
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
m n : ℕ
⊢ ⌊↑m / ↑n⌋₊ = m / n
convert floor_div_nat (m : α) n
no goals
case h.e'_3.h.e'_5
F : Type ?u.97534
α : Type u_1
β : Type ?u.97540
inst✝¹ : LinearOrderedSemifield α
inst✝ : FloorSemiring α
m n : ℕ
⊢ m = ⌊↑m⌋₊
rw [m.floor_coe]