Documentation

Mathlib.Init.Data.Nat.Basic

def Nat.recC {motive : ℕ → Sort u} (zero : motive Nat.zero) (succ : (n : ℕ) → motive n → motive (Nat.succ n)) (t : ℕ) :

motive t

A computable version of Nat.rec. Workaround until Lean has native support for this.

Equations

Nat.recC zero succ 0 = zero
Nat.recC zero succ (Nat.succ n) = succ n (Nat.recC zero succ n)

@[csimp]

theorem Nat.rec_eq_recC :

@Nat.rec = @Nat.recC

theorem Nat.bit0_succ_eq (n : ℕ) :

bit0 (Nat.succ n) = Nat.succ (Nat.succ (bit0 n))

theorem Nat.zero_lt_bit0 {n : ℕ} :

n ≠ 0 → 0 < bit0 n

theorem Nat.zero_lt_bit1 (n : ℕ) :

0 < bit1 n

theorem Nat.bit0_ne_zero {n : ℕ} :

n ≠ 0 → bit0 n ≠ 0

theorem Nat.bit1_ne_zero (n : ℕ) :