F x = If x < 10 then x else F (x - 1)

みたいな関数ってCoqでどう性質を証明しますか？ifの条件で場合分けしたいです

タクティックでcase ( x< 10)としても、
仮説にならないで、場合わけにならずに困っています。