Theorem: trunc_le_trunc_of_lt_next_trunc (Fl/Trunc.lean)

State before:
n x y : ℕ
npos : 0 < n
h : x < next n (trunc n y)
⊢ trunc n x ≤ trunc n y
Tactic:
cases Nat.le_total x (trunc n y) with
| inl hxy => exact trunc_le_trunc npos (Nat.le_trans hxy (trunc_le n y))
| inr hyx => exact ge_of_eq (trunc_eq_trunc_of_le_of_lt npos hyx h)
State after:
no goals

State before:
case inl
n x y : ℕ
npos : 0 < n
h : x < next n (trunc n y)
hxy : x ≤ trunc n y
⊢ trunc n x ≤ trunc n y
Tactic:
exact trunc_le_trunc npos (Nat.le_trans hxy (trunc_le n y))
State after:
no goals

State before:
case inr
n x y : ℕ
npos : 0 < n
h : x < next n (trunc n y)
hyx : trunc n y ≤ x
⊢ trunc n x ≤ trunc n y
Tactic:
exact ge_of_eq (trunc_eq_trunc_of_le_of_lt npos hyx h)
State after:
no goals