gen_as.lean:7:2: proof state
x y : ℕ
⊢ ∀ n,
    n ≥ 0