{ 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₂⟩
  simp only [propagateCarry_propagateCarry_add] at h₁
  rcases have _wf : n - (b - a) < n :=
     Nat.sub_lt (lt_of_lt_of_le (pow_pos (by norm_num) _) (le_of_not_lt hn2)) (Nat.sub_pos_of_lt h₂)
    exists_repeat (λ c i => if i < a + (n - 2 ^ card α) then seq c i else
      seq c (i + (b - a))) (n - (b - a)) with ⟨m, hmle, seq2, hm⟩
  use m; use hmle; use seq2
  rw [hm]; clear hm
  have h1 : n - (b - a) = (a + (n - 2 ^ (card α))) + (2 ^ card α - b) := by
  { zify
    rw [Nat.cast_sub, Nat.cast_sub, Nat.cast_sub, Nat.cast_sub]
    ring_nf
    exact Nat.le_of_lt_succ b.2
    simp [*] at *
    exact hn2
    exact le_of_lt h₂
    exact le_trans (Nat.sub_le _ _) (le_trans (Nat.le_of_lt_succ b.2)
      (le_of_not_lt hn2)) }
  rw [h1]
  have h2 : n = (b + (n - 2 ^ card α)) + (2 ^ card α - b) := by
  { zify
    rw [Nat.cast_sub, Nat.cast_sub]
    ring
    exact Nat.le_of_lt_succ b.2
    simp [*] at *
    exact hn2 }
  conv_rhs => rw [h2]
  refine' propagate_eq_of_carry_eq _ _ _ _ _ _ _ _ _
  { 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 }
    rw [← h₁]
    apply propagateCarry2_eq_of_seq_eq_lt
    simp (config := { contextual := true }) }
  { intro y c _hc
    simp only [add_lt_iff_neg_left, not_lt_zero', if_false]
    congr 1
    zify
    rw [Nat.cast_sub, Nat.cast_sub]
    ring
    exact le_of_lt h₂
    exact le_of_not_lt hn2 } }
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
no goals