Theorem: density (Test/Real/Density.lean)

State before:
x z : ℝ
⊢ x < z → ∃ y, x < y ∧ y < z
Tactic:
sorry
State after:
no goals