case intro
α : Type ?u.244025
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ Nat.dist n m ≤ 1
α : Type ?u.244025
n m : ℕ
H : Raised n m
⊢ Nat.dist n m ≤ 1
cases' raised_iff.1 H with H1 H2
no goals
case intro
α : Type ?u.244025
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ Nat.dist n m ≤ 1
rwa [Nat.dist_eq_sub_of_le H1, tsub_le_iff_left]