calc
  a = trunc n a             := by rw [hfa]
  _ ≤ trunc n (2 * (a - b)) := trunc_le_trunc npos h
  _ = 2 * trunc n (a - b)   := by rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
  _ ≤ 2 * round (a - b)     := Nat.mul_le_mul_left _ (trunc_le_round n _ hfaithful₁)
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ a ≤ 2 * round (a - b)
no goals