rewrite [Nat.two_mul] at hab
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ 2 * b
⊢ trunc n (a - b) = a - b
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ trunc n (a - b) = a - b