no goals
α✝ : Type ?u.230327
β : Type ?u.230330
γ : Type ?u.230333
f g : α✝ → β
c c₁ c₂ x : α✝
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ fract (a + 1) = fract a
exact_mod_cast Int.fract_add_int a 1