@[simp]

theorem NatPair.pair_zero {m : ℕ} : pair 0 m = m * 2

@[simp]

theorem NatPair.fst_mul_two {n : ℕ} : fst (n * 2) = 0

@[simp]

theorem NatPair.fst_pair {n m : ℕ} : fst (pair n m) = n

@[simp]

theorem NatPair.pair_add_one {n m : ℕ} : pair n m + 1 = 2 ^ n * (m * 2 + 1)

@[simp]

theorem NatPair.snd_pair {n m : ℕ} : snd (pair n m) = m

@[simp]

theorem NatPair.odd_add_one_div_two_pow_fst {n : ℕ} : Odd ((n + 1) / 2 ^ fst n)

@[simp]

theorem NatPair.two_pow_fst_le_succ {n : ℕ} : 2 ^ fst n ≤ n + 1

@[simp]

theorem NatPair.two_pow_fst_mul_sub_one_eq_self {n : ℕ} : 2 ^ fst n * ((n + 1) / 2 ^ fst n) - 1 = n

@[simp]

theorem NatPair.pair_fst_snd {r : ℕ} : pair (fst r) (snd r) = r

@[simp]

theorem NatPair.leftInverse_g_f : Function.LeftInverse g f

@[simp]

theorem NatPair.rightInverse_g_f : Function.RightInverse g f