eSHP.first_gap_odd_gt_1

lemma first_gap_odd_gt_1 {g : ℕ} (hg : Odd g) (hg1 : 1 < g) : first_gap g = 0 := by  simp only [first_gap, dite_eq_right_iff, forall_exists_index]  intro n hn  obtain ⟨k, hk⟩ := hg  simp_all only [lt_add_iff_pos_left, ofNat_pos, mul_pos_iff_of_pos_left]  have : ∀ n > 0, Odd (nth_prime n) := fun n hn ↦ Prime.odd_of_ne_two (prime_nth_prime n) (by    grind [Prime.two_le (prime_nth_prime n),      show nth_prime n > 2 from lt_of_le_of_lt (Prime.two_le <| prime_nth_prime 0) <|        nth_strictMono infinite_setOf_prime hn])  have : Even (nth_prime (n + 1) - nth_prime n) :=    Nat.Odd.sub_odd (this _ n.succ_pos) <| this n (pos_of_ne_zero (by      rintro rfl; unfold nth_prime_gap at hn; aesop))  aesop