Theorem: from_above (BrownCs22/Demos/01-intro.lean)

State before:
p q r : Prop
⊢ ∀ (x : ℕ), ∃ y, x < y
Tactic:
sorry
State after:
no goals