Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Prototypes.Computability.BitTree.Elias.CodeBits

set_option doc.verso true

Fixed-width binary countdown

Digits are stored least significant first, with leading zeroes retained. Decrement propagates a borrow through the initial zeroes and clears the first one. At zero it wraps within the existing width; numeric correctness is therefore stated for positive inputs.

Main definitions

value interprets a list of binary digits.
decrement preserves the width while subtracting one.
borrowFlips counts the digits changed by a borrow.

Main statements

length_decrement states width preservation.
value_decrement gives the numeric meaning for positive counter values.

Tags

binary counter, decrement, borrow, fixed width

@[expose] public sectionnamespace Geb.BitTree.Elias.Counter

Interpret binary digits, allowing leading zeroes.

def value (bs : List Bool) : ℕ := bs.foldr Nat.bit 0

Adding a least significant digit doubles the value and adds that digit.

theorem value_cons (b : Bool) (bs : List Bool) :
    value (b :: bs) = 2 * value bs + b.toNat := Nat.bit_val b (value bs)

Canonical binary digits represent the number from which they were obtained.

theorem value_bits (n : ℕ) : value n.bits = n := foldr_bits n

A binary word represents zero exactly when all its digits are zero.

theorem value_eq_zero_iff (bs : List Bool) : value bs = 0 ↔ ∀ b ∈ bs, b = false := bybs:List Bool⊢ value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false
  apply List.rec (motive := fun bs ↦ value bs = 0 ↔ ∀ b ∈ bs, b = false) ?_ ?_ bsbs:List Bool⊢ value [] = 0 ↔ ∀ (b : Bool), b ∈ [] → b = falsebs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (value tail = 0 ↔ ∀ (b : Bool), b ∈ tail → b = false) →
    (value (head :: tail) = 0 ↔ ∀ (b : Bool), b ∈ head :: tail → b = false)
  ·bs:List Bool⊢ value [] = 0 ↔ ∀ (b : Bool), b ∈ [] → b = false simp [value]All goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (value tail = 0 ↔ ∀ (b : Bool), b ∈ tail → b = false) →
    (value (head :: tail) = 0 ↔ ∀ (b : Bool), b ∈ head :: tail → b = false) intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ value (b :: bs) = 0 ↔ ∀ (b_1 : Bool), b_1 ∈ b :: bs → b_1 = false
    rw [value_cons,bs✝:List Boolb:Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + b.toNat = 0 ↔ ∀ (b_1 : Bool), b_1 ∈ b :: bs → b_1 = false List.forall_mem_consbs✝:List Boolb:Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + b.toNat = 0 ↔ b = false ∧ ∀ (x : Bool), x ∈ bs → x = false]bs✝:List Boolb:Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + b.toNat = 0 ↔ b = false ∧ ∀ (x : Bool), x ∈ bs → x = false
    cases bfalsebs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + false.toNat = 0 ↔ false = false ∧ ∀ (x : Bool), x ∈ bs → x = falsetruebs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + true.toNat = 0 ↔ true = false ∧ ∀ (x : Bool), x ∈ bs → x = false
    ·falsebs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + false.toNat = 0 ↔ false = false ∧ ∀ (x : Bool), x ∈ bs → x = false simp only [Bool.toNat_false]falsebs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + 0 = 0 ↔ True ∧ ∀ (x : Bool), x ∈ bs → x = false
      constructorfalse.mpbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + 0 = 0 → True ∧ ∀ (x : Bool), x ∈ bs → x = falsefalse.mprbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ (True ∧ ∀ (x : Bool), x ∈ bs → x = false) → 2 * value bs + 0 = 0
      ·false.mpbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + 0 = 0 → True ∧ ∀ (x : Bool), x ∈ bs → x = false intro hfalse.mpbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = falseh:2 * value bs + 0 = 0⊢ True ∧ ∀ (x : Bool), x ∈ bs → x = false
        exact ⟨trivial, ih.mp (bybs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = falseh:2 * value bs + 0 = 0⊢ value bs = 0 omegaAll goals completed! 🐙)⟩
      ·false.mprbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ (True ∧ ∀ (x : Bool), x ∈ bs → x = false) → 2 * value bs + 0 = 0 rintro ⟨_, h⟩false.mprbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = falseleft✝:Trueh:∀ (x : Bool), x ∈ bs → x = false⊢ 2 * value bs + 0 = 0
        have ht := ih.mpr hfalse.mprbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = falseleft✝:Trueh:∀ (x : Bool), x ∈ bs → x = falseht:value bs = 0⊢ 2 * value bs + 0 = 0
        omegaAll goals completed! 🐙
    ·truebs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + true.toNat = 0 ↔ true = false ∧ ∀ (x : Bool), x ∈ bs → x = false simp only [Bool.toNat_true]truebs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + 1 = 0 ↔ true = false ∧ ∀ (x : Bool), x ∈ bs → x = false
      constructortrue.mpbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + 1 = 0 → true = false ∧ ∀ (x : Bool), x ∈ bs → x = falsetrue.mprbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ (true = false ∧ ∀ (x : Bool), x ∈ bs → x = false) → 2 * value bs + 1 = 0
      ·true.mpbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ 2 * value bs + 1 = 0 → true = false ∧ ∀ (x : Bool), x ∈ bs → x = false intro htrue.mpbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = falseh:2 * value bs + 1 = 0⊢ true = false ∧ ∀ (x : Bool), x ∈ bs → x = false
        omegaAll goals completed! 🐙
      ·true.mprbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = false⊢ (true = false ∧ ∀ (x : Bool), x ∈ bs → x = false) → 2 * value bs + 1 = 0 rintro ⟨h, _⟩true.mprbs✝:List Boolbs:List Boolih:value bs = 0 ↔ ∀ (b : Bool), b ∈ bs → b = falseh:true = falseright✝:∀ (x : Bool), x ∈ bs → x = false⊢ 2 * value bs + 1 = 0
        cases hAll goals completed! 🐙

The usual boolean test for an all-zero word agrees with its numeric value.

theorem all_not_eq_true_iff (bs : List Bool) :
    bs.all (fun b ↦ !b) = true ↔ value bs = 0 := bybs:List Bool⊢ (bs.all fun b ↦ !b) = true ↔ value bs = 0
  rw [value_eq_zero_iff,bs:List Bool⊢ (bs.all fun b ↦ !b) = true ↔ ∀ (b : Bool), b ∈ bs → b = false List.all_eq_truebs:List Bool⊢ (∀ (x : Bool), x ∈ bs → (!x) = true) ↔ ∀ (b : Bool), b ∈ bs → b = false]bs:List Bool⊢ (∀ (x : Bool), x ∈ bs → (!x) = true) ↔ ∀ (b : Bool), b ∈ bs → b = false
  constructormpbs:List Bool⊢ (∀ (x : Bool), x ∈ bs → (!x) = true) → ∀ (b : Bool), b ∈ bs → b = falsemprbs:List Bool⊢ (∀ (b : Bool), b ∈ bs → b = false) → ∀ (x : Bool), x ∈ bs → (!x) = true
  ·mpbs:List Bool⊢ (∀ (x : Bool), x ∈ bs → (!x) = true) → ∀ (b : Bool), b ∈ bs → b = false intro h b hbmpbs:List Boolh:∀ (x : Bool), x ∈ bs → (!x) = trueb:Boolhb:b ∈ bs⊢ b = false
    have he := h b hbmpbs:List Boolh:∀ (x : Bool), x ∈ bs → (!x) = trueb:Boolhb:b ∈ bshe:(!b) = true⊢ b = false
    cases bmp.falsebs:List Boolh:∀ (x : Bool), x ∈ bs → (!x) = truehb:false ∈ bshe:(!false) = true⊢ false = falsemp.truebs:List Boolh:∀ (x : Bool), x ∈ bs → (!x) = truehb:true ∈ bshe:(!true) = true⊢ true = false
    ·mp.falsebs:List Boolh:∀ (x : Bool), x ∈ bs → (!x) = truehb:false ∈ bshe:(!false) = true⊢ false = false rflAll goals completed! 🐙
    ·mp.truebs:List Boolh:∀ (x : Bool), x ∈ bs → (!x) = truehb:true ∈ bshe:(!true) = true⊢ true = false cases heAll goals completed! 🐙
  ·mprbs:List Bool⊢ (∀ (b : Bool), b ∈ bs → b = false) → ∀ (x : Bool), x ∈ bs → (!x) = true intro h b hbmprbs:List Boolh:∀ (b : Bool), b ∈ bs → b = falseb:Boolhb:b ∈ bs⊢ (!b) = true
    rw [h b hbmprbs:List Boolh:∀ (b : Bool), b ∈ bs → b = falseb:Boolhb:b ∈ bs⊢ (!false) = true]mprbs:List Boolh:∀ (b : Bool), b ∈ bs → b = falseb:Boolhb:b ∈ bs⊢ (!false) = true
    rflAll goals completed! 🐙

Recording whether any digit is one detects a zero counter.

theorem any_eq_false_iff (bs : List Bool) : bs.any id = false ↔ value bs = 0 := bybs:List Bool⊢ bs.any id = false ↔ value bs = 0
  rw [List.any_eq_false,bs:List Bool⊢ (∀ (x : Bool), x ∈ bs → ¬id x = true) ↔ value bs = 0 value_eq_zero_iffbs:List Bool⊢ (∀ (x : Bool), x ∈ bs → ¬id x = true) ↔ ∀ (b : Bool), b ∈ bs → b = false]bs:List Bool⊢ (∀ (x : Bool), x ∈ bs → ¬id x = true) ↔ ∀ (b : Bool), b ∈ bs → b = false
  constructormpbs:List Bool⊢ (∀ (x : Bool), x ∈ bs → ¬id x = true) → ∀ (b : Bool), b ∈ bs → b = falsemprbs:List Bool⊢ (∀ (b : Bool), b ∈ bs → b = false) → ∀ (x : Bool), x ∈ bs → ¬id x = true
  ·mpbs:List Bool⊢ (∀ (x : Bool), x ∈ bs → ¬id x = true) → ∀ (b : Bool), b ∈ bs → b = false intro h b hbmpbs:List Boolh:∀ (x : Bool), x ∈ bs → ¬id x = trueb:Boolhb:b ∈ bs⊢ b = false
    have hn := h b hbmpbs:List Boolh:∀ (x : Bool), x ∈ bs → ¬id x = trueb:Boolhb:b ∈ bshn:¬id b = true⊢ b = false
    cases bmp.falsebs:List Boolh:∀ (x : Bool), x ∈ bs → ¬id x = truehb:false ∈ bshn:¬id false = true⊢ false = falsemp.truebs:List Boolh:∀ (x : Bool), x ∈ bs → ¬id x = truehb:true ∈ bshn:¬id true = true⊢ true = false
    ·mp.falsebs:List Boolh:∀ (x : Bool), x ∈ bs → ¬id x = truehb:false ∈ bshn:¬id false = true⊢ false = false rflAll goals completed! 🐙
    ·mp.truebs:List Boolh:∀ (x : Bool), x ∈ bs → ¬id x = truehb:true ∈ bshn:¬id true = true⊢ true = false exact False.elim (hn rfl)All goals completed! 🐙
  ·mprbs:List Bool⊢ (∀ (b : Bool), b ∈ bs → b = false) → ∀ (x : Bool), x ∈ bs → ¬id x = true intro h b hbmprbs:List Boolh:∀ (b : Bool), b ∈ bs → b = falseb:Boolhb:b ∈ bs⊢ ¬id b = true
    rw [h b hbmprbs:List Boolh:∀ (b : Bool), b ∈ bs → b = falseb:Boolhb:b ∈ bs⊢ ¬id false = true]mprbs:List Boolh:∀ (b : Bool), b ∈ bs → b = falseb:Boolhb:b ∈ bs⊢ ¬id false = true
    intro hemprbs:List Boolh:∀ (b : Bool), b ∈ bs → b = falseb:Boolhb:b ∈ bshe:id false = true⊢ False
    cases heAll goals completed! 🐙

Subtract one within the existing width, wrapping an all-zero word.

def decrement : List Bool → List Bool :=
  List.rec [] fun b bs next ↦ if b then false :: bs else true :: next

Count the initial zeroes and the first one, or the whole width at zero.

def borrowFlips : List Bool → ℕ :=
  List.foldr (fun b n ↦ if b then 1 else n + 1) 0

Decrement never changes the allocated width.

theorem length_decrement (bs : List Bool) : (decrement bs).length = bs.length := bybs:List Bool⊢ (decrement bs).length = bs.length
  apply List.rec (motive := fun bs ↦ (decrement bs).length = bs.length) ?_ ?_ bsbs:List Bool⊢ (decrement []).length = [].lengthbs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (decrement tail).length = tail.length → (decrement (head :: tail)).length = (head :: tail).length
  ·bs:List Bool⊢ (decrement []).length = [].length rflAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (decrement tail).length = tail.length → (decrement (head :: tail)).length = (head :: tail).length intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:(decrement bs).length = bs.length⊢ (decrement (b :: bs)).length = (b :: bs).length
    cases bfalsebs✝:List Boolbs:List Boolih:(decrement bs).length = bs.length⊢ (decrement (false :: bs)).length = (false :: bs).lengthtruebs✝:List Boolbs:List Boolih:(decrement bs).length = bs.length⊢ (decrement (true :: bs)).length = (true :: bs).length <;>falsebs✝:List Boolbs:List Boolih:(decrement bs).length = bs.length⊢ (decrement (false :: bs)).length = (false :: bs).lengthtruebs✝:List Boolbs:List Boolih:(decrement bs).length = bs.length⊢ (decrement (true :: bs)).length = (true :: bs).length simp_all [decrement]All goals completed! 🐙

A borrow changes at most the allocated width.

theorem borrowFlips_le_length (bs : List Bool) : borrowFlips bs ≤ bs.length := bybs:List Bool⊢ borrowFlips bs ≤ bs.length
  apply List.rec (motive := fun bs ↦ borrowFlips bs ≤ bs.length) ?_ ?_ bsbs:List Bool⊢ borrowFlips [] ≤ [].lengthbs:List Bool⊢ ∀ (head : Bool) (tail : List Bool), borrowFlips tail ≤ tail.length → borrowFlips (head :: tail) ≤ (head :: tail).length
  ·bs:List Bool⊢ borrowFlips [] ≤ [].length exact Nat.le_refl _All goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool), borrowFlips tail ≤ tail.length → borrowFlips (head :: tail) ≤ (head :: tail).length intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:borrowFlips bs ≤ bs.length⊢ borrowFlips (b :: bs) ≤ (b :: bs).length
    cases bfalsebs✝:List Boolbs:List Boolih:borrowFlips bs ≤ bs.length⊢ borrowFlips (false :: bs) ≤ (false :: bs).lengthtruebs✝:List Boolbs:List Boolih:borrowFlips bs ≤ bs.length⊢ borrowFlips (true :: bs) ≤ (true :: bs).length <;>falsebs✝:List Boolbs:List Boolih:borrowFlips bs ≤ bs.length⊢ borrowFlips (false :: bs) ≤ (false :: bs).lengthtruebs✝:List Boolbs:List Boolih:borrowFlips bs ≤ bs.length⊢ borrowFlips (true :: bs) ≤ (true :: bs).length simp_all [borrowFlips]All goals completed! 🐙

Decrement subtracts one from every positive represented value.

theorem value_decrement (bs : List Bool) (h : 0 < value bs) :
    value (decrement bs) = value bs - 1 := bybs:List Boolh:0 < value bs⊢ value (decrement bs) = value bs - 1
  revert hbs:List Bool⊢ 0 < value bs → value (decrement bs) = value bs - 1
  apply List.rec (motive := fun bs ↦ 0 < value bs →
    value (decrement bs) = value bs - 1) ?_ ?_ bsbs:List Bool⊢ 0 < value [] → value (decrement []) = value [] - 1bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (0 < value tail → value (decrement tail) = value tail - 1) →
    0 < value (head :: tail) → value (decrement (head :: tail)) = value (head :: tail) - 1
  ·bs:List Bool⊢ 0 < value [] → value (decrement []) = value [] - 1 intro hbs:List Boolh:0 < value []⊢ value (decrement []) = value [] - 1
    exact (Nat.not_lt_zero 0 h).elimAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (0 < value tail → value (decrement tail) = value tail - 1) →
    0 < value (head :: tail) → value (decrement (head :: tail)) = value (head :: tail) - 1 intro b bs ih hbs✝:List Boolb:Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (b :: bs)⊢ value (decrement (b :: bs)) = value (b :: bs) - 1
    cases bfalsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)⊢ value (decrement (false :: bs)) = value (false :: bs) - 1truebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (true :: bs)⊢ value (decrement (true :: bs)) = value (true :: bs) - 1
    ·falsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)⊢ value (decrement (false :: bs)) = value (false :: bs) - 1 have hp : 0 < value bs := bybs:List Boolh:0 < value bs⊢ value (decrement bs) = value bs - 1
        rw [value_consbs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < 2 * value bs + false.toNat⊢ 0 < value bs] at hbs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < 2 * value bs + false.toNat⊢ 0 < value bs
        simp only [Bool.toNat_false] at hbs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < 2 * value bs + 0⊢ 0 < value bs
        omegafalsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)hp:0 < value bs⊢ value (decrement (false :: bs)) = value (false :: bs) - 1
      change value (true :: decrement bs) = value (false :: bs) - 1falsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)hp:0 < value bs⊢ value (true :: decrement bs) = value (false :: bs) - 1
      rw [value_cons,falsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)hp:0 < value bs⊢ 2 * value (decrement bs) + true.toNat = value (false :: bs) - 1 value_cons,falsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)hp:0 < value bs⊢ 2 * value (decrement bs) + true.toNat = 2 * value bs + false.toNat - 1 ih hpfalsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)hp:0 < value bs⊢ 2 * (value bs - 1) + true.toNat = 2 * value bs + false.toNat - 1]falsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)hp:0 < value bs⊢ 2 * (value bs - 1) + true.toNat = 2 * value bs + false.toNat - 1
      simp only [Bool.toNat_true, Bool.toNat_false]falsebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (false :: bs)hp:0 < value bs⊢ 2 * (value bs - 1) + 1 = 2 * value bs + 0 - 1
      omegaAll goals completed! 🐙
    ·truebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (true :: bs)⊢ value (decrement (true :: bs)) = value (true :: bs) - 1 change value (false :: bs) = value (true :: bs) - 1truebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (true :: bs)⊢ value (false :: bs) = value (true :: bs) - 1
      rw [value_cons,truebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (true :: bs)⊢ 2 * value bs + false.toNat = value (true :: bs) - 1 value_construebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (true :: bs)⊢ 2 * value bs + false.toNat = 2 * value bs + true.toNat - 1]truebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (true :: bs)⊢ 2 * value bs + false.toNat = 2 * value bs + true.toNat - 1
      simp only [Bool.toNat_true, Bool.toNat_false]truebs✝:List Boolbs:List Boolih:0 < value bs → value (decrement bs) = value bs - 1h:0 < value (true :: bs)⊢ 2 * value bs + 0 = 2 * value bs + 1 - 1
      omegaAll goals completed! 🐙

A positive counter requires at least one changed digit.

theorem borrowFlips_pos (bs : List Bool) (h : 0 < value bs) : 0 < borrowFlips bs := bybs:List Boolh:0 < value bs⊢ 0 < borrowFlips bs
  cases bs with
  | nil =>nilh:0 < value []⊢ 0 < borrowFlips [] exact (Nat.not_lt_zero 0 h).elimAll goals completed! 🐙
  | cons b bs =>consb:Boolbs:List Boolh:0 < value (b :: bs)⊢ 0 < borrowFlips (b :: bs) cases bcons.falsebs:List Boolh:0 < value (false :: bs)⊢ 0 < borrowFlips (false :: bs)cons.truebs:List Boolh:0 < value (true :: bs)⊢ 0 < borrowFlips (true :: bs) <;>cons.falsebs:List Boolh:0 < value (false :: bs)⊢ 0 < borrowFlips (false :: bs)cons.truebs:List Boolh:0 < value (true :: bs)⊢ 0 < borrowFlips (true :: bs) simp [borrowFlips]All goals completed! 🐙

Every digit before the final changed position is zero.

theorem getD_eq_false_of_lt_borrowFlips (bs : List Bool) (i : ℕ)
    (h : i + 1 < borrowFlips bs) : bs[i]?.getD false = false := bybs:List Booli:ℕh:i + 1 < borrowFlips bs⊢ bs[i]?.getD false = false
  revert ibs:List Bool⊢ ∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = false
  apply List.rec (motive := fun bs ↦ ∀ i, i + 1 < borrowFlips bs →
    bs[i]?.getD false = false) ?_ ?_ bsbs:List Bool⊢ ∀ (i : ℕ), i + 1 < borrowFlips [] → [][i]?.getD false = falsebs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (i : ℕ), i + 1 < borrowFlips tail → tail[i]?.getD false = false) →
    ∀ (i : ℕ), i + 1 < borrowFlips (head :: tail) → (head :: tail)[i]?.getD false = false
  ·bs:List Bool⊢ ∀ (i : ℕ), i + 1 < borrowFlips [] → [][i]?.getD false = false intro i _bs:List Booli:ℕa✝:i + 1 < borrowFlips []⊢ [][i]?.getD false = false
    rflAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (i : ℕ), i + 1 < borrowFlips tail → tail[i]?.getD false = false) →
    ∀ (i : ℕ), i + 1 < borrowFlips (head :: tail) → (head :: tail)[i]?.getD false = false intro b bs ih i hibs✝:List Boolb:Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 < borrowFlips (b :: bs)⊢ (b :: bs)[i]?.getD false = false
    cases bfalsebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 < borrowFlips (false :: bs)⊢ (false :: bs)[i]?.getD false = falsetruebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 < borrowFlips (true :: bs)⊢ (true :: bs)[i]?.getD false = false
    ·falsebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 < borrowFlips (false :: bs)⊢ (false :: bs)[i]?.getD false = false cases i with
      | zero =>false.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsehi:0 + 1 < borrowFlips (false :: bs)⊢ (false :: bs)[0]?.getD false = false rflAll goals completed! 🐙
      | succ i =>false.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 + 1 < borrowFlips (false :: bs)⊢ (false :: bs)[i + 1]?.getD false = false
        change bs[i]?.getD false = falsefalse.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 + 1 < borrowFlips (false :: bs)⊢ bs[i]?.getD false = false
        apply ihfalse.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 + 1 < borrowFlips (false :: bs)⊢ i + 1 < borrowFlips bs
        change i + 1 + 1 < borrowFlips bs + 1 at hifalse.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 + 1 < borrowFlips bs + 1⊢ i + 1 < borrowFlips bs
        omegaAll goals completed! 🐙
    ·truebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 < borrowFlips (true :: bs)⊢ (true :: bs)[i]?.getD false = false change i + 1 < 1 at hitruebs✝:List Boolbs:List Boolih:∀ (i : ℕ), i + 1 < borrowFlips bs → bs[i]?.getD false = falsei:ℕhi:i + 1 < 1⊢ (true :: bs)[i]?.getD false = false
      omegaAll goals completed! 🐙

The final changed position of a positive counter contains one.

theorem getD_last_borrowFlips (bs : List Bool) (h : 0 < value bs) :
    bs[borrowFlips bs - 1]?.getD false = true := bybs:List Boolh:0 < value bs⊢ bs[borrowFlips bs - 1]?.getD false = true
  revert hbs:List Bool⊢ 0 < value bs → bs[borrowFlips bs - 1]?.getD false = true
  apply List.rec (motive := fun bs ↦ 0 < value bs →
    bs[borrowFlips bs - 1]?.getD false = true) ?_ ?_ bsbs:List Bool⊢ 0 < value [] → [][borrowFlips [] - 1]?.getD false = truebs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (0 < value tail → tail[borrowFlips tail - 1]?.getD false = true) →
    0 < value (head :: tail) → (head :: tail)[borrowFlips (head :: tail) - 1]?.getD false = true
  ·bs:List Bool⊢ 0 < value [] → [][borrowFlips [] - 1]?.getD false = true intro hbs:List Boolh:0 < value []⊢ [][borrowFlips [] - 1]?.getD false = true
    exact (Nat.not_lt_zero 0 h).elimAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (0 < value tail → tail[borrowFlips tail - 1]?.getD false = true) →
    0 < value (head :: tail) → (head :: tail)[borrowFlips (head :: tail) - 1]?.getD false = true intro b bs ih hbs✝:List Boolb:Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (b :: bs)⊢ (b :: bs)[borrowFlips (b :: bs) - 1]?.getD false = true
    cases bfalsebs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (false :: bs)⊢ (false :: bs)[borrowFlips (false :: bs) - 1]?.getD false = truetruebs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (true :: bs)⊢ (true :: bs)[borrowFlips (true :: bs) - 1]?.getD false = true
    ·falsebs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (false :: bs)⊢ (false :: bs)[borrowFlips (false :: bs) - 1]?.getD false = true have hp : 0 < value bs := bybs:List Boolh:0 < value bs⊢ bs[borrowFlips bs - 1]?.getD false = true
        rw [value_consbs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < 2 * value bs + false.toNat⊢ 0 < value bs] at hbs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < 2 * value bs + false.toNat⊢ 0 < value bs
        simp only [Bool.toNat_false] at hbs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < 2 * value bs + 0⊢ 0 < value bs
        omegafalsebs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (false :: bs)hp:0 < value bs⊢ (false :: bs)[borrowFlips (false :: bs) - 1]?.getD false = true
      have hf := borrowFlips_pos bs hpfalsebs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (false :: bs)hp:0 < value bshf:0 < borrowFlips bs⊢ (false :: bs)[borrowFlips (false :: bs) - 1]?.getD false = true
      have he : borrowFlips (false :: bs) - 1 = (borrowFlips bs - 1) + 1 := bybs:List Boolh:0 < value bs⊢ bs[borrowFlips bs - 1]?.getD false = true
        change borrowFlips bs + 1 - 1 = borrowFlips bs - 1 + 1bs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (false :: bs)hp:0 < value bshf:0 < borrowFlips bs⊢ borrowFlips bs + 1 - 1 = borrowFlips bs - 1 + 1
        omegafalsebs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (false :: bs)hp:0 < value bshf:0 < borrowFlips bshe:borrowFlips (false :: bs) - 1 = borrowFlips bs - 1 + 1⊢ (false :: bs)[borrowFlips (false :: bs) - 1]?.getD false = true
      simpa only [he, List.getElem?_cons_succ] using ih hpAll goals completed! 🐙
    ·truebs✝:List Boolbs:List Boolih:0 < value bs → bs[borrowFlips bs - 1]?.getD false = trueh:0 < value (true :: bs)⊢ (true :: bs)[borrowFlips (true :: bs) - 1]?.getD false = true rflAll goals completed! 🐙

Decrement flips exactly the initial borrow positions, preserving all later digits.

theorem getD_decrement (bs : List Bool) (i : ℕ) :
    (decrement bs)[i]?.getD false =
      if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD false := bybs:List Booli:ℕ⊢ (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD false
  revert ibs:List Bool⊢ ∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD false
  apply List.rec (motive := fun bs ↦ ∀ i,
    (decrement bs)[i]?.getD false =
      if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD false) ?_ ?_ bsbs:List Bool⊢ ∀ (i : ℕ), (decrement [])[i]?.getD false = if i < borrowFlips [] then ![][i]?.getD false else [][i]?.getD falsebs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (i : ℕ),
      (decrement tail)[i]?.getD false = if i < borrowFlips tail then !tail[i]?.getD false else tail[i]?.getD false) →
    ∀ (i : ℕ),
      (decrement (head :: tail))[i]?.getD false =
        if i < borrowFlips (head :: tail) then !(head :: tail)[i]?.getD false else (head :: tail)[i]?.getD false
  ·bs:List Bool⊢ ∀ (i : ℕ), (decrement [])[i]?.getD false = if i < borrowFlips [] then ![][i]?.getD false else [][i]?.getD false intro ibs:List Booli:ℕ⊢ (decrement [])[i]?.getD false = if i < borrowFlips [] then ![][i]?.getD false else [][i]?.getD false
    change false = if i < 0 then true else falsebs:List Booli:ℕ⊢ false = if i < 0 then true else false
    simp only [show ¬i < 0 from by omega, ↓reduceIte]All goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  (∀ (i : ℕ),
      (decrement tail)[i]?.getD false = if i < borrowFlips tail then !tail[i]?.getD false else tail[i]?.getD false) →
    ∀ (i : ℕ),
      (decrement (head :: tail))[i]?.getD false =
        if i < borrowFlips (head :: tail) then !(head :: tail)[i]?.getD false else (head :: tail)[i]?.getD false intro b bs ih ibs✝:List Boolb:Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ (decrement (b :: bs))[i]?.getD false =
  if i < borrowFlips (b :: bs) then !(b :: bs)[i]?.getD false else (b :: bs)[i]?.getD false
    cases bfalsebs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ (decrement (false :: bs))[i]?.getD false =
  if i < borrowFlips (false :: bs) then !(false :: bs)[i]?.getD false else (false :: bs)[i]?.getD falsetruebs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ (decrement (true :: bs))[i]?.getD false =
  if i < borrowFlips (true :: bs) then !(true :: bs)[i]?.getD false else (true :: bs)[i]?.getD false
    ·falsebs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ (decrement (false :: bs))[i]?.getD false =
  if i < borrowFlips (false :: bs) then !(false :: bs)[i]?.getD false else (false :: bs)[i]?.getD false cases i with
      | zero =>false.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD false⊢ (decrement (false :: bs))[0]?.getD false =
  if 0 < borrowFlips (false :: bs) then !(false :: bs)[0]?.getD false else (false :: bs)[0]?.getD false
        change true = if 0 < borrowFlips bs + 1 then true else falsefalse.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD false⊢ true = if 0 < borrowFlips bs + 1 then true else false
        simp only [show 0 < borrowFlips bs + 1 from by omega, ↓reduceIte]All goals completed! 🐙
      | succ i =>false.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ (decrement (false :: bs))[i + 1]?.getD false =
  if i + 1 < borrowFlips (false :: bs) then !(false :: bs)[i + 1]?.getD false else (false :: bs)[i + 1]?.getD false
        change (decrement bs)[i]?.getD false =
          if i + 1 < borrowFlips bs + 1 then !bs[i]?.getD false else bs[i]?.getD falsefalse.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ (decrement bs)[i]?.getD false = if i + 1 < borrowFlips bs + 1 then !bs[i]?.getD false else bs[i]?.getD false
        have he : (i + 1 < borrowFlips bs + 1) ↔ (i < borrowFlips bs) := bybs:List Booli:ℕ⊢ (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD false
          constructormpbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ i + 1 < borrowFlips bs + 1 → i < borrowFlips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ i < borrowFlips bs → i + 1 < borrowFlips bs + 1 <;>mpbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ i + 1 < borrowFlips bs + 1 → i < borrowFlips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ i < borrowFlips bs → i + 1 < borrowFlips bs + 1 intro hmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕh:i < borrowFlips bs⊢ i + 1 < borrowFlips bs + 1 <;>mpbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕh:i + 1 < borrowFlips bs + 1⊢ i < borrowFlips bsmprbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕh:i < borrowFlips bs⊢ i + 1 < borrowFlips bs + 1 omegafalse.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕhe:i + 1 < borrowFlips bs + 1 ↔ i < borrowFlips bs⊢ (decrement bs)[i]?.getD false = if i + 1 < borrowFlips bs + 1 then !bs[i]?.getD false else bs[i]?.getD false
        simpa only [he] using ih iAll goals completed! 🐙
    ·truebs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ (decrement (true :: bs))[i]?.getD false =
  if i < borrowFlips (true :: bs) then !(true :: bs)[i]?.getD false else (true :: bs)[i]?.getD false cases i with
      | zero =>true.zerobs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD false⊢ (decrement (true :: bs))[0]?.getD false =
  if 0 < borrowFlips (true :: bs) then !(true :: bs)[0]?.getD false else (true :: bs)[0]?.getD false rflAll goals completed! 🐙
      | succ i =>true.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ (decrement (true :: bs))[i + 1]?.getD false =
  if i + 1 < borrowFlips (true :: bs) then !(true :: bs)[i + 1]?.getD false else (true :: bs)[i + 1]?.getD false
        change bs[i]?.getD false =
          if i + 1 < 1 then !bs[i]?.getD false else bs[i]?.getD falsetrue.succbs✝:List Boolbs:List Boolih:∀ (i : ℕ), (decrement bs)[i]?.getD false = if i < borrowFlips bs then !bs[i]?.getD false else bs[i]?.getD falsei:ℕ⊢ bs[i]?.getD false = if i + 1 < 1 then !bs[i]?.getD false else bs[i]?.getD false
        simp only [show ¬i + 1 < 1 from by omega, ↓reduceIte]All goals completed! 🐙

The zero-digit potential pays for a borrow even when zero wraps to all ones.

theorem borrowFlips_add_count_decrement_le (bs : List Bool) :
    borrowFlips bs + (decrement bs).count false ≤ bs.count false + 2 := bybs:List Bool⊢ borrowFlips bs + List.count false (decrement bs) ≤ List.count false bs + 2
  apply List.rec (motive := fun bs ↦
    borrowFlips bs + (decrement bs).count false ≤ bs.count false + 2) ?_ ?_ bsbs:List Bool⊢ borrowFlips [] + List.count false (decrement []) ≤ List.count false [] + 2bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  borrowFlips tail + List.count false (decrement tail) ≤ List.count false tail + 2 →
    borrowFlips (head :: tail) + List.count false (decrement (head :: tail)) ≤ List.count false (head :: tail) + 2
  ·bs:List Bool⊢ borrowFlips [] + List.count false (decrement []) ≤ List.count false [] + 2 decideAll goals completed! 🐙
  ·bs:List Bool⊢ ∀ (head : Bool) (tail : List Bool),
  borrowFlips tail + List.count false (decrement tail) ≤ List.count false tail + 2 →
    borrowFlips (head :: tail) + List.count false (decrement (head :: tail)) ≤ List.count false (head :: tail) + 2 intro b bs ihbs✝:List Boolb:Boolbs:List Boolih:borrowFlips bs + List.count false (decrement bs) ≤ List.count false bs + 2⊢ borrowFlips (b :: bs) + List.count false (decrement (b :: bs)) ≤ List.count false (b :: bs) + 2
    cases bfalsebs✝:List Boolbs:List Boolih:borrowFlips bs + List.count false (decrement bs) ≤ List.count false bs + 2⊢ borrowFlips (false :: bs) + List.count false (decrement (false :: bs)) ≤ List.count false (false :: bs) + 2truebs✝:List Boolbs:List Boolih:borrowFlips bs + List.count false (decrement bs) ≤ List.count false bs + 2⊢ borrowFlips (true :: bs) + List.count false (decrement (true :: bs)) ≤ List.count false (true :: bs) + 2 <;>falsebs✝:List Boolbs:List Boolih:borrowFlips bs + List.count false (decrement bs) ≤ List.count false bs + 2⊢ borrowFlips (false :: bs) + List.count false (decrement (false :: bs)) ≤ List.count false (false :: bs) + 2truebs✝:List Boolbs:List Boolih:borrowFlips bs + List.count false (decrement bs) ≤ List.count false bs + 2⊢ borrowFlips (true :: bs) + List.count false (decrement (true :: bs)) ≤ List.count false (true :: bs) + 2 simp_all [decrement, borrowFlips]truebs✝:List Boolbs:List Boolih:List.foldr (fun b n ↦ if b = true then 1 else n + 1) 0 bs +
    List.count false (List.rec [] (fun b bs next ↦ if b = true then false :: bs else true :: next) bs) ≤
  List.count false bs + 2⊢ 1 + (List.count false bs + 1) ≤ List.count false bs + 2 <;>falsebs✝:List Boolbs:List Boolih:List.foldr (fun b n ↦ if b = true then 1 else n + 1) 0 bs +
    List.count false (List.rec [] (fun b bs next ↦ if b = true then false :: bs else true :: next) bs) ≤
  List.count false bs + 2⊢ List.foldr (fun b n ↦ if b = true then 1 else n + 1) 0 bs + 1 +
    List.count false (List.rec [] (fun b bs next ↦ if b = true then false :: bs else true :: next) bs) ≤
  List.count false bs + 1 + 2truebs✝:List Boolbs:List Boolih:List.foldr (fun b n ↦ if b = true then 1 else n + 1) 0 bs +
    List.count false (List.rec [] (fun b bs next ↦ if b = true then false :: bs else true :: next) bs) ≤
  List.count false bs + 2⊢ 1 + (List.count false bs + 1) ≤ List.count false bs + 2 omegaAll goals completed! 🐙

end Geb.BitTree.Elias.Counter