/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura
-/
import Mathlib.Init.ZeroOne
import Mathlib.Init.Data.Nat.Notation
import Mathlib.Util.CompileInductive

namespace Nat

set_option linter.deprecated false

protected theorem bit0_succ_eq: ∀ (n : ℕ), bit0 (succ n) = succ (succ (bit0 n))
bit0_succ_eq (n: ℕ
n : ℕ: Type
ℕ) : bit0: {α : Type ?u.5} → [inst : Add α] → α → α
bit0 (succ: ℕ → ℕ
succ n: ℕ
n) = succ: ℕ → ℕ
succ (succ: ℕ → ℕ
succ (bit0: {α : Type ?u.10} → [inst : Add α] → α → α
bit0 n: ℕ
n)) :=
  show succ: ℕ → ℕ
succ (succ: ℕ → ℕ
succ n: ℕ
n + n: ℕ
n) = succ: ℕ → ℕ
succ (succ: ℕ → ℕ
succ (n: ℕ
n + n: ℕ
n)) from congrArg: ∀ {α : Sort ?u.88} {β : Sort ?u.87} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congrArg succ: ℕ → ℕ
succ (succ_add: ∀ (n m : ℕ), succ n + m = succ (n + m)
succ_add n: ℕ
n n: ℕ
n)
#align nat.bit0_succ_eq Nat.bit0_succ_eq: ∀ (n : ℕ), bit0 (succ n) = succ (succ (bit0 n))
Nat.bit0_succ_eq

protected theorem zero_lt_bit0: ∀ {n : ℕ}, n ≠ 0 → 0 < bit0 n
zero_lt_bit0 : ∀ {n: ℕ
n : Nat: Type
Nat}, n: ℕ
n ≠ 0: ?m.114
0 → 0: ?m.126
0 < bit0: {α : Type ?u.139} → [inst : Add α] → α → α
bit0 n: ℕ
n
  | 0: ℕ
0, h: 0 ≠ 0
h => absurd: ∀ {a : Prop} {b : Sort ?u.180}, a → ¬a → b
absurd rfl: ∀ {α : Sort ?u.183} {a : α}, a = a
rfl h: 0 ≠ 0
h
  | succ: ℕ → ℕ
succ n: ℕ
n, _ =>
    calc
      0: ?m.211
0 < succ: ℕ → ℕ
succ (succ: ℕ → ℕ
succ (bit0: {α : Type ?u.224} → [inst : Add α] → α → α
bit0 n: ℕ
n)) := zero_lt_succ: ∀ (n : ℕ), 0 < succ n
zero_lt_succ _: ℕ
_
      _: ?m✝
_ = bit0: {α : Type ?u.259} → [inst : Add α] → α → α
bit0 (succ: ℕ → ℕ
succ n: ℕ
n) := (Nat.bit0_succ_eq: ∀ (n : ℕ), bit0 (succ n) = succ (succ (bit0 n))
Nat.bit0_succ_eq n: ℕ
n).symm: ∀ {α : Sort ?u.263} {a b : α}, a = b → b = a
symm
#align nat.zero_lt_bit0 Nat.zero_lt_bit0: ∀ {n : ℕ}, n ≠ 0 → 0 < bit0 n
Nat.zero_lt_bit0

protected theorem zero_lt_bit1: ∀ (n : ℕ), 0 < bit1 n
zero_lt_bit1 (n: ℕ
n : Nat: Type
Nat) : 0: ?m.443
0 < bit1: {α : Type ?u.456} → [inst : One α] → [inst : Add α] → α → α
bit1 n: ℕ
n :=
  zero_lt_succ: ∀ (n : ℕ), 0 < succ n
zero_lt_succ _: ℕ
_
#align nat.zero_lt_bit1 Nat.zero_lt_bit1: ∀ (n : ℕ), 0 < bit1 n
Nat.zero_lt_bit1

protected theorem bit0_ne_zero: ∀ {n : ℕ}, n ≠ 0 → bit0 n ≠ 0
bit0_ne_zero : ∀ {n: ℕ
n : ℕ: Type
ℕ}, n: ℕ
n ≠ 0: ?m.513
0 → bit0: {α : Type ?u.525} → [inst : Add α] → α → α
bit0 n: ℕ
n ≠ 0: ?m.533
0
  | 0: ℕ
0, h: 0 ≠ 0
h => absurd: ∀ {a : Prop} {b : Sort ?u.563}, a → ¬a → b
absurd rfl: ∀ {α : Sort ?u.566} {a : α}, a = a
rfl h: 0 ≠ 0
h
  | n: ℕ
n + 1, _ =>
    suffices n: ℕ
n + 1: ?m.668
1 + (n: ℕ
n + 1: ?m.681
1) ≠ 0: ?m.753
0 from this: n + 1 + (n + 1) ≠ 0
this
    suffices succ: ℕ → ℕ
succ (n: ℕ
n + 1: ?m.765
1 + n: ℕ
n) ≠ 0: ?m.819
0 from this: succ (n + 1 + n) ≠ 0
this
    fun h: ?m.822
h => Nat.noConfusion: ∀ {P : Sort ?u.824} {v1 v2 : ℕ}, v1 = v2 → Nat.noConfusionType P v1 v2
Nat.noConfusion h: ?m.822
h
#align nat.bit0_ne_zero Nat.bit0_ne_zero: ∀ {n : ℕ}, n ≠ 0 → bit0 n ≠ 0
Nat.bit0_ne_zero

protected theorem bit1_ne_zero: ∀ (n : ℕ), bit1 n ≠ 0
bit1_ne_zero (n: ℕ
n : ℕ: Type
ℕ) : bit1: {α : Type ?u.980} → [inst : One α] → [inst : Add α] → α → α
bit1 n: ℕ
n ≠ 0: ?m.1011
0 :=
  show succ: ℕ → ℕ
succ (n: ℕ
n + n: ℕ
n) ≠ 0: ?m.1056
0 from fun h: ?m.1071
h => Nat.noConfusion: ∀ {P : Sort ?u.1073} {v1 v2 : ℕ}, v1 = v2 → Nat.noConfusionType P v1 v2
Nat.noConfusion h: ?m.1071
h
#align nat.bit1_ne_zero Nat.bit1_ne_zero: ∀ (n : ℕ), bit1 n ≠ 0
Nat.bit1_ne_zero

end Nat