rcases exists_repeat_carry
  (propagateCarry2 init_carry (λ c b => (next_bit c b).1) seq
    (n - 2 ^ card α))
  (λ carry bits => (next_bit  carry bits).1)
  (λ b i => seq b (i + (n - 2^ (card α)))) with ⟨a, b, h₁, h₂⟩
case neg
α β α' β' : 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 α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
case neg.intro.intro.intro
α β α' β' : 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₁ :
  propagateCarry2 (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (n - 2 ^ card α))
      (fun carry bits => (next_bit carry bits).fst) (fun b i => seq b (i + (n - 2 ^ card α))) ↑a =
    propagateCarry2 (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (n - 2 ^ card α))
      (fun carry bits => (next_bit carry bits).fst) (fun b i => seq b (i + (n - 2 ^ card α))) ↑b
h₂ : a < b
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n