n : ℕ
v : Bitvec n
this : Bitvec.toNat v + 1 ≤ 2 ^ n
⊢ Bitvec.toNat v < 2 ^ n

case this
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v + 1 ≤ 2 ^ n
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v < 2 ^ n
suffices : v.toNat + 1 ≤ 2 ^ n
case this
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v + 1 ≤ 2 ^ n
n : ℕ
v : Bitvec n
this : Bitvec.toNat v + 1 ≤ 2 ^ n
⊢ Bitvec.toNat v < 2 ^ n

case this
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v + 1 ≤ 2 ^ n
simpa
case this
n : ℕ
v : Bitvec n
⊢ List.foldr (flip addLsb) 0 (List.reverse (Vector.toList v)) + 1 ≤ 2 ^ n
case this
n : ℕ
v : Bitvec n
⊢ Bitvec.toNat v + 1 ≤ 2 ^ n
rw [toNat_eq_foldr_reverse]
case this.mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ List.foldr (flip addLsb) 0 (List.reverse (Vector.toList { val := xs, property := h })) + 1 ≤ 2 ^ n
case this
n : ℕ
v : Bitvec n
⊢ List.foldr (flip addLsb) 0 (List.reverse (Vector.toList v)) + 1 ≤ 2 ^ n
cases' v with xs h
case this.mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ List.foldr (flip addLsb) 0 (List.reverse xs) + 1 ≤ 2 ^ n
case this.mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ List.foldr (flip addLsb) 0 (List.reverse (Vector.toList { val := xs, property := h })) + 1 ≤ 2 ^ n
dsimp [Bitvec.toNat, bitsToNat]
case this.mk
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ List.foldr (flip addLsb) 0 (List.reverse xs) + 1 ≤ 2 ^ n
case this.mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ List.foldr (flip addLsb) 0 (List.reverse xs) + 1 ≤ 2 ^ n
rw [← List.length_reverse] at h
case this.mk
n : ℕ
xs ys : List Bool
h : List.length ys = n
⊢ List.foldr (flip addLsb) 0 ys + 1 ≤ 2 ^ n
case this.mk
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ List.foldr (flip addLsb) 0 (List.reverse xs) + 1 ≤ 2 ^ n
generalize xs.reverse = ys at h
case this.mk.nil
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
n : ℕ
h : List.length [] = n
⊢ List.foldr (flip addLsb) 0 [] + 1 ≤ 2 ^ n

case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ List.foldr (flip addLsb) 0 (head :: tail) + 1 ≤ 2 ^ n
case this.mk
n : ℕ
xs ys : List Bool
h : List.length ys = n
⊢ List.foldr (flip addLsb) 0 ys + 1 ≤ 2 ^ n
induction' ys with head tail ih generalizing n
no goals
case this.mk.nil
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
n : ℕ
h : List.length [] = n
⊢ List.foldr (flip addLsb) 0 [] + 1 ≤ 2 ^ n
simp [← h]
case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ addLsb (List.foldr (fun b a => addLsb a b) 0 tail) head + 1 ≤ 2 ^ List.length tail * 2
case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ List.foldr (flip addLsb) 0 (head :: tail) + 1 ≤ 2 ^ n
simp only [← h, pow_add, flip, List.length, List.foldr, pow_one]
case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (2 * List.foldr (fun b a => addLsb a b) 0 tail + bif head then 1 else 0) + 1 ≤ 2 ^ List.length tail * 2
case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ addLsb (List.foldr (fun b a => addLsb a b) 0 tail) head + 1 ≤ 2 ^ List.length tail * 2
rw [addLsb_eq_twice_add_one]
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (2 * List.foldr (fun b a => addLsb a b) 0 tail + bif head then 1 else 0) + 1 ≤
    2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1

n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1 ≤ 2 ^ List.length tail * 2
case this.mk.cons
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (2 * List.foldr (fun b a => addLsb a b) 0 tail + bif head then 1 else 0) + 1 ≤ 2 ^ List.length tail * 2
trans 2 * List.foldr (fun (x : Bool) (y : ℕ) => addLsb y x) 0 tail + 2 * 1
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * List.foldr (fun b a => addLsb a b) 0 tail + ((bif head then 1 else 0) + 1) ≤
    2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (2 * List.foldr (fun b a => addLsb a b) 0 tail + bif head then 1 else 0) + 1 ≤
    2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1
rw [add_assoc]
case h
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (bif head then 1 else 0) + 1 ≤ 2 * 1
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * List.foldr (fun b a => addLsb a b) 0 tail + ((bif head then 1 else 0) + 1) ≤
    2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1
apply Nat.add_le_add_left
no goals
case h
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ (bif head then 1 else 0) + 1 ≤ 2 * 1
cases head <;> simp only
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * (List.foldr (fun x y => addLsb y x) 0 tail + 1) ≤ 2 ^ List.length tail * 2
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * List.foldr (fun x y => addLsb y x) 0 tail + 2 * 1 ≤ 2 ^ List.length tail * 2
rw [← left_distrib]
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * (List.foldr (fun x y => addLsb y x) 0 tail + 1) ≤ 2 * 2 ^ List.length tail
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * (List.foldr (fun x y => addLsb y x) 0 tail + 1) ≤ 2 ^ List.length tail * 2
rw [mul_comm _ 2]
case h
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ List.foldr (fun x y => addLsb y x) 0 tail + 1 ≤ 2 ^ List.length tail
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ 2 * (List.foldr (fun x y => addLsb y x) 0 tail + 1) ≤ 2 * 2 ^ List.length tail
apply Nat.mul_le_mul_left
no goals
case h
n✝ : ℕ
xs ys : List Bool
h✝ : List.length ys = n✝
head : Bool
tail : List Bool
ih : ∀ {n : ℕ}, List.length tail = n → List.foldr (flip addLsb) 0 tail + 1 ≤ 2 ^ n
n : ℕ
h : List.length (head :: tail) = n
⊢ List.foldr (fun x y => addLsb y x) 0 tail + 1 ≤ 2 ^ List.length tail
exact ih rfl