Theorem: trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq (Fl/Trunc.lean)

State before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ trunc n (x - 1) = x - ulp n (x - 1)
Tactic:
unfold trunc
State after:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ (x - 1) / ulp n (x - 1) * ulp n (x - 1) = x - ulp n (x - 1)

State before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ (x - 1) / ulp n (x - 1) * ulp n (x - 1) = x - ulp n (x - 1)
Tactic:
apply div_mul_pred_eq_sub_of_pos_of_dvd
State after:
case h₀
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < ulp n (x - 1)

case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x

State before:
case h₀
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < ulp n (x - 1)

case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Tactic:
. exact ulp_pos n _
State after:
case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x

State before:
case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x

case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Tactic:
. exact xpos
State after:
case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x

State before:
case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Tactic:
. trans ulp n x
  . exact ulp_dvd_ulp n tsub_le_self
  . exact ulp_dvd_of_trunc_eq hfx
State after:
no goals

State before:
case h₀
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < ulp n (x - 1)
Tactic:
exact ulp_pos n _
State after:
no goals

State before:
case h₂
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ 0 < x
Tactic:
exact xpos
State after:
no goals

State before:
case h₁
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ x
Tactic:
trans ulp n x
State after:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ ulp n x

x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x

State before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ ulp n x

x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x
Tactic:
. exact ulp_dvd_ulp n tsub_le_self
State after:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x

State before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x
Tactic:
. exact ulp_dvd_of_trunc_eq hfx
State after:
no goals

State before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n (x - 1) ∣ ulp n x
Tactic:
exact ulp_dvd_ulp n tsub_le_self
State after:
no goals

State before:
x n : ℕ
xpos : 0 < x
hfx : trunc n x = x
⊢ ulp n x ∣ x
Tactic:
exact ulp_dvd_of_trunc_eq hfx
State after:
no goals