Theorem: float_greatest_m_exists (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
x : ℝ
m : ℤ
⊢ x ≠ 0 → greatest_m fmt x = ↑m → is_greatest_m fmt x m ∧ 1 ≤ m ∧ m < (↑fmt).r
Tactic:
sorry
State after:
no goals