feat: @[simp] Nat.count / Nat.nth of fun _ ↦ True, False (#13378)
@[simp]
Nat.count
Nat.nth
fun _ ↦ True
False