4051.lean:9:8-9:26: warning: declaration uses `sorry`