Theorem: trunc_pred_eq_trunc_of_trunc_ne_self (Fl/Trunc.lean)

State before:
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n (a - 1) = trunc n a
Tactic:
symm
State after:
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a = trunc n (a - 1)

State before:
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a = trunc n (a - 1)
Tactic:
apply trunc_eq_trunc_of_le_of_lt npos
State after:
case h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a ≤ a - 1

case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)

State before:
case h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a ≤ a - 1

case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)
Tactic:
. apply Nat.le_pred_of_lt
  exact Nat.lt_of_le_of_ne (trunc_le n a) h
State after:
case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)

State before:
case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)
Tactic:
. exact Nat.lt_of_le_of_lt tsub_le_self (lt_next_trunc npos a)
State after:
no goals

State before:
case h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a ≤ a - 1
Tactic:
apply Nat.le_pred_of_lt
State after:
case h.h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a < Nat.sub a 0

State before:
case h.h
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ trunc n a < Nat.sub a 0
Tactic:
exact Nat.lt_of_le_of_ne (trunc_le n a) h
State after:
no goals

State before:
case k
n a : ℕ
npos : 0 < n
h : trunc n a ≠ a
⊢ a - 1 < next n (trunc n a)
Tactic:
exact Nat.lt_of_le_of_lt tsub_le_self (lt_next_trunc npos a)
State after:
no goals