Theorem: natRealCoeLtCoe (FromTheBook/Ch02/Bertrand/Bertrand.lean)

State before:
a b : ℕ
⊢ ↑a < ↑b ↔ a < b
Tactic:
simp
State after:
no goals