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

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