Theorem: next_trunc_pred_trunc_eq_self (Fl/Trunc.lean)

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ next n (trunc n (trunc n x - 1)) = trunc n x
Tactic:
symm
State after:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = next n (trunc n (trunc n x - 1))

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = next n (trunc n (trunc n x - 1))
Tactic:
rewrite [← trunc_next_comm npos (trunc n x - 1)]
State after:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (next n (trunc n x - 1))

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (next n (trunc n x - 1))
Tactic:
unfold next
State after:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (trunc n x - 1 + ulp n (trunc n x - 1))

State before:
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x = trunc n (trunc n x - 1 + ulp n (trunc n x - 1))
Tactic:
apply trunc_eq_trunc_of_le_of_lt npos
State after:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x ≤ trunc n x - 1 + ulp n (trunc n x - 1)

case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)

State before:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x ≤ trunc n x - 1 + ulp n (trunc n x - 1)

case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
Tactic:
. rewrite [← tsub_le_iff_right]
  apply tsub_le_tsub_left
  exact Nat.one_le_of_lt (ulp_pos _ _)
State after:
case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)

State before:
case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
Tactic:
. apply add_lt_add_of_lt_of_le
  . exact tsub_lt_self xpos zero_lt_one
  . exact ulp_le_ulp n tsub_le_self
State after:
no goals

State before:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x ≤ trunc n x - 1 + ulp n (trunc n x - 1)
Tactic:
rewrite [← tsub_le_iff_right]
State after:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - ulp n (trunc n x - 1) ≤ trunc n x - 1

State before:
case h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - ulp n (trunc n x - 1) ≤ trunc n x - 1
Tactic:
apply tsub_le_tsub_left
State after:
case h.h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ 1 ≤ ulp n (trunc n x - 1)

State before:
case h.h
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ 1 ≤ ulp n (trunc n x - 1)
Tactic:
exact Nat.one_le_of_lt (ulp_pos _ _)
State after:
no goals

State before:
case k
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 + ulp n (trunc n x - 1) < next n (trunc n x)
Tactic:
apply add_lt_add_of_lt_of_le
State after:
case k.h₁
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 < trunc n x

case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)

State before:
case k.h₁
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 < trunc n x

case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)
Tactic:
. exact tsub_lt_self xpos zero_lt_one
State after:
case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)

State before:
case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)
Tactic:
. exact ulp_le_ulp n tsub_le_self
State after:
no goals

State before:
case k.h₁
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ trunc n x - 1 < trunc n x
Tactic:
exact tsub_lt_self xpos zero_lt_one
State after:
no goals

State before:
case k.h₂
n x : ℕ
npos : 0 < n
xpos : 0 < trunc n x
⊢ ulp n (trunc n x - 1) ≤ ulp n (trunc n x)
Tactic:
exact ulp_le_ulp n tsub_le_self
State after:
no goals