[math-fun] An identity involving the floor function