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
xs : ℕ → A
zero_case : xs 0 = x
incr_case : ∀ (n : ℕ), R (xs n) (xs (n + 1))
⊢ R (xs 0) (xs 1)
no goals