Library HoTT.Foundations.MLTT.Nat
This file is part of https://github.com/mjub/hott.
Inductive β : πβ := zero | succ : β β β.
Notation "0" := zero.
Notation "n + 1" := (succ n)
(at level 2, left associativity, format "n + 1").
Notation "n + 2" := (succ (succ n))
(at level 2, left associativity, format "n + 2").
Notation "n + 3" := (succ (succ (succ n)))
(at level 2, left associativity, format "n + 3").
Elimination principles for the natural numbers.
Fixpoint ind_β (C : β β π) (cβ : C 0) (cβ : β n, C n β C (n + 1)) n :=
match n with
| 0 β cβ
| k + 1 β cβ k (ind_β _ cβ cβ k)
end.
Fixpoint rec_β {C : π} (cβ : C) (cβ : β n, C β C) n :=
match n with
| 0 β cβ
| k + 1 β cβ k (rec_β cβ cβ k)
end.