match div_x with
  | Exists.intro xs (And.intro zero_case incr_case) =>
  apply norm_x (xs 1)
  rw [←zero_case]
  apply incr_case
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
⊢ False
no goals