Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
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 :
ℕ: Type
ℕ
) :
bit0: {α : Type ?u.5} → [inst : Add α] → α → α
bit0
(
succ: ℕ → ℕ
succ
n) =
succ: ℕ → ℕ
succ
(
succ: ℕ → ℕ
succ
(
bit0: {α : Type ?u.10} → [inst : Add α] → α → α
bit0
n)) := show
succ: ℕ → ℕ
succ
(
succ: ℕ → ℕ
succ
n + n) =
succ: ℕ → ℕ
succ
(
succ: ℕ → ℕ
succ
(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) #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 :
Nat: Type
Nat
}, n ≠
0: ?m.114
0
→
0: ?m.126
0
<
bit0: {α : Type ?u.139} → [inst : Add α] → α → α
bit0
n | 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, _ => calc
0: ?m.211
0
<
succ: ℕ → ℕ
succ
(
succ: ℕ → ℕ
succ
(
bit0: {α : Type ?u.224} → [inst : Add α] → α → α
bit0
n)) :=
zero_lt_succ: ∀ (n : ℕ), 0 < succ n
zero_lt_succ
_
_: ?m✝
_
=
bit0: {α : Type ?u.259} → [inst : Add α] → α → α
bit0
(
succ: ℕ → ℕ
succ
n) := (
Nat.bit0_succ_eq: ∀ (n : ℕ), bit0 (succ n) = succ (succ (bit0 n))
Nat.bit0_succ_eq
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 :
Nat: Type
Nat
) :
0: ?m.443
0
<
bit1: {α : Type ?u.456} → [inst : One α] → [inst : Add α] → α → α
bit1
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 :
ℕ: Type
ℕ
}, n ≠
0: ?m.513
0
→
bit0: {α : Type ?u.525} → [inst : Add α] → α → α
bit0
n ≠
0: ?m.533
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 + 1, _ => suffices n +
1: ?m.668
1
+ (n +
1: ?m.681
1
) ≠
0: ?m.753
0
from
this: n + 1 + (n + 1) ≠ 0
this
suffices
succ: ℕ → ℕ
succ
(n +
1: ?m.765
1
+ 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 :
ℕ: Type
ℕ
) :
bit1: {α : Type ?u.980} → [inst : One α] → [inst : Add α] → α → α
bit1
n ≠
0: ?m.1011
0
:= show
succ: ℕ → ℕ
succ
(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