C : FloatCfg
⊢ emin ≤ emin + (↑prec - 1)
C : FloatCfg
⊢ emin ≤ emin + ↑prec - 1
rw [add_sub_assoc]
case h
C : FloatCfg
⊢ 0 ≤ ↑prec - 1
C : FloatCfg
⊢ emin ≤ emin + (↑prec - 1)
apply le_add_of_nonneg_right
case h.a
C : FloatCfg
⊢ 1 ≤ ↑prec
case h
C : FloatCfg
⊢ 0 ≤ ↑prec - 1
apply sub_nonneg_of_le
case h.a.a
C : FloatCfg
⊢ 1 ≤ prec
case h.a
C : FloatCfg
⊢ 1 ≤ ↑prec
apply Int.ofNat_le_ofNat_of_le
no goals
case h.a.a
C : FloatCfg
⊢ 1 ≤ prec
exact C.precPos
C : FloatCfg
this : ↑prec ≤ ↑(2 * emax)
⊢ emin + ↑prec - 1 ≤ ↑emax
C : FloatCfg
this : prec ≤ 2 * emax
⊢ emin + ↑prec - 1 ≤ ↑emax
rw [← Int.ofNat_le] at this
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * emax)
this : 0 ≤ ↑(2 * emax) - ↑prec
⊢ 0 ≤ ↑emax - (emin + ↑prec - 1)
C : FloatCfg
this : ↑prec ≤ ↑(2 * emax)
⊢ emin + ↑prec - 1 ≤ ↑emax
rw [← sub_nonneg] at *
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax - (1 - ↑FloatCfg.emax + ↑prec - 1)
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * emax)
this : 0 ≤ ↑(2 * emax) - ↑prec
⊢ 0 ≤ ↑emax - (emin + ↑prec - 1)
simp only [emin, emax] at *
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax * 2 - ↑prec
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax - (1 - ↑FloatCfg.emax + ↑prec - 1)
ring_nf
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ 2 * ↑FloatCfg.emax - ↑prec
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax * 2 - ↑prec
rw [mul_comm]
no goals
C : FloatCfg
this✝ : ↑prec ≤ ↑(2 * FloatCfg.emax)
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ 2 * ↑FloatCfg.emax - ↑prec
assumption
no goals
C : FloatCfg
⊢ 0 < 2
decide
no goals
C : FloatCfg
⊢ emin = max (emin + ↑(Nat.size 0) - ↑prec) emin
(rw [max_eq_right]; simp [sub_eq_add_neg])
C : FloatCfg
⊢ emin + ↑(Nat.size 0) - ↑prec ≤ emin
C : FloatCfg
⊢ emin = max (emin + ↑(Nat.size 0) - ↑prec) emin
rw [max_eq_right]
no goals
C : FloatCfg
⊢ emin + ↑(Nat.size 0) - ↑prec ≤ emin
simp [sub_eq_add_neg]