Documentation

Mathlib.Init.Data.Nat.Basic

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

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

Equations
theorem Nat.zero_lt_bit0 {n : } :
n 00 < bit0 n
theorem Nat.zero_lt_bit1 (n : ) :
0 < bit1 n
theorem Nat.bit0_ne_zero {n : } :
n 0bit0 n 0