intro y c _hc
case neg.intro.intro.intro.intro.intro.intro.refine'_2
α β α' β' : 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)
⊢ ∀ (y : ℕ) (b_1 : β),
    y ≤ 2 ^ card α - ↑b →
      (if ↑a + (n - 2 ^ card α) + y < ↑a + (n - 2 ^ card α) then seq b_1 (↑a + (n - 2 ^ card α) + y)
        else seq b_1 (↑a + (n - 2 ^ card α) + y + (↑b - ↑a))) =
        seq b_1 (↑b + (n - 2 ^ card α) + y)
case neg.intro.intro.intro.intro.intro.intro.refine'_2
α β α' β' : 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)
y : ℕ
c : β
_hc : y ≤ 2 ^ card α - ↑b
⊢ (if ↑a + (n - 2 ^ card α) + y < ↑a + (n - 2 ^ card α) then seq c (↑a + (n - 2 ^ card α) + y)
    else seq c (↑a + (n - 2 ^ card α) + y + (↑b - ↑a))) =
    seq c (↑b + (n - 2 ^ card α) + y)