have _h : ↑b + (n - 2 ^ card α) = (a + (n - 2 ^ card α)) + (b - a) := by
{ zify
  rw [Nat.cast_sub, Nat.cast_sub]
  ring_nf
  exact le_of_lt h₂
  exact le_of_not_lt hn2 }
case neg.intro.intro.intro.intro.intro.intro.refine'_1
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
h2 : n = ↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst)
      (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a))) (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq (↑b + (n - 2 ^ card α))
case neg.intro.intro.intro.intro.intro.intro.refine'_1
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
h2 : n = ↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b)
_h : ↑b + (n - 2 ^ card α) = ↑a + (n - 2 ^ card α) + (↑b - ↑a)
⊢ propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst)
      (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a))) (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq (↑b + (n - 2 ^ card α))