Ks_eq_zero_of_le_dist

lemma Ks_eq_zero_of_le_dist {s : ℤ} {x y : X} (h : D ^ s / 2 ≤ dist x y) : Ks s x y = 0 := by  have hxy : x ≠ y := by    rw [← dist_pos]    apply lt_of_lt_of_le _ h    simp only [Nat.ofNat_pos, div_pos_iff_of_pos_right]    exact defaultD_pow_pos a s  rw [Ks_def]  simp only [mul_eq_zero, ofReal_eq_zero]  right  rw [psi_eq_zero_iff (one_lt_realD (X := X)) (dist_pos.mpr hxy),    mem_nonzeroS_iff (one_lt_realD (X := X)) (dist_pos.mpr hxy)]  simp only [mem_Ioo, not_and_or, not_lt]  right  rw [zpow_neg, le_inv_mul_iff₀ (defaultD_pow_pos a s)]  exact h