@[simp]

theorem RealEquiv.Bits.get_cons {bs : Bits} {b : Bit} : (bs.cons b).get = fun (i : ℕ) => if i = 0 then b else bs.get (i - 1)

@[simp]

theorem RealEquiv.Bits.get_drop {bs : Bits} {n : ℕ} : (bs.drop n).get = fun (i : ℕ) => bs.get (n + i)

@[simp]

theorem RealEquiv.Bits.get_tail {bs : Bits} : bs.tail.get = fun (i : ℕ) => bs.get (i + 1)

@[simp]

theorem RealEquiv.Bits.cons_tail_get_zero {bs : Bits} : bs.tail.cons (bs.get 0) = bs

theorem RealEquiv.Bits.cs {P : Bits → Prop} (h : ∀ ⦃b : Bit⦄ ⦃bs : Bits⦄, P (bs.cons b)) (bs : Bits) : P bs

@[simp]

theorem RealEquiv.Bits.tail_cons {bs : Bits} {b : Bit} : (bs.cons b).tail = bs

@[simp]

theorem RealEquiv.Bits.end_cons {bs : Bits} {b : Bit} : (bs.cons b).end = bs.end

@[simp]

theorem RealEquiv.Bits.end_drop {bs : Bits} {n : ℕ} : (bs.drop n).end = bs.end

@[simp]

theorem RealEquiv.Bits.end_tail {bs : Bits} : bs.tail.end = bs.end

theorem RealEquiv.Bits.end_eq_of_getNat {bs bs₁ : Bits} {n : ℕ} (h : bs.getNat = (n, bs₁)) : bs₁.end = bs.end

@[simp]

theorem RealEquiv.prepend_nil {bs : Bits} : bs.prepend [] = bs

@[simp]

theorem RealEquiv.prepend_cons {bs : Bits} {b : Bit} {xs : List Bit} : bs.prepend (b :: xs) = (bs.prepend xs).cons b

@[simp]

theorem RealEquiv.Bits.get_prepend {bs : Bits} {xs : List Bit} : (bs.prepend xs).get = fun (i : ℕ) => if h : i < xs.length then xs[i] else bs.get (i - xs.length)

theorem RealEquiv.Bits.eq_prepend_of_end_eq_none {bs : Bits} (h : bs.end = none) (b : Bit) : ∃ (n : ℕ), ((bs.drop (n + 1)).cons b).prepend (List.replicate n b.not) = bs

@[simp]

theorem RealEquiv.Bits.take_sub {bs : Bits} {n k : ℕ} : bs.take (n - k) = List.take (n - k) (bs.take n)

@[simp]

theorem RealEquiv.Bits.length_take {bs : Bits} {n : ℕ} : (bs.take n).length = n