(or (or (= n zero) (positive n)) (negative n))

Theorem: The tripartition property about integers.

(or (elem n nat) (not (elem n nat)))

Theorem: An alternative split principle for integers (or a constructive excluded middle principle, so to speak).

A

Theorem: An elimination princile for integers, cf. int-split-elim-rule.

(forall
 [n int]
 (==> (==> (= n zero) A) (==> (positive n) A) (==> (negative n) A) A))

Theorem: An elimination principle for integers.

(or (= n zero) (not (= n zero)))

Theorem: Yet another split principle for integers.

(lambda
 [x int]
 (forall
  [P (==> int :type)]
  (==> (and (P zero) (nat-succ-prop P)) (P x))))

Definition: The subset of natural integers.

(==>
 (P zero)
 (forall-in [k nat] (P (succ k)))
 (forall-in [n nat] (P n)))

Theorem: Case analysis for natural numbers.

(==>
 (P zero)
 (forall [x int] (==> (elem x nat) (P x) (P (succ x))))
 (forall [x int] (==> (elem x nat) (P x))))

Theorem: The induction principle for natural integers. This is the third Peano axiom but it can be derived from int-induct.

(forall-in [n nat] (or (= n zero) (positive n)))

Theorem: A natural number is either zero or it is positive

(==> (elem x nat) (elem (succ x) nat))

Theorem: The successor of a natural integer is a natural integer.

(forall
 [x y int]
 (==> (elem x nat) (elem y nat) (= (succ x) (succ y)) (= x y)))

Theorem: Successor is injective, the second Peano ‘axiom’ here a simple consequence of succ-injective.

(forall [y int] (==> (P y) (P (succ y))))

Definition: A property verified by all successors of natural integers.

(elem zero nat)

Theorem: Zero is a natural integer.

(not (elem (pred zero) nat))

Axiom: An important axiom of the natural integer subset wrt. pred.

(forall [x int] (==> (elem x nat) (not (= (succ x) zero))))

Theorem: Zero is not a successor of a natural integer.

This is the first Peano ‘axiom’ (here theorem, based on integers) for natural integers.

(not (elem n nat))

Definition: The integer n is strictly negative.

(forall-in [n nat] (not (negative n)))

Theorem:

(not (negative zero))

Theorem:

(==> (negative n) (negative (pred n)))

Theorem: Negative predecessors.

(==> (negative (pred n)) (or (= n zero) (negative n)))

Theorem: Splitting of a predecessor.

(==> (or (= n zero) (negative n)) (negative (pred n)))

Theorem: An auxiliary theorem for the predecessor.

(<=> (negative (pred n)) (or (= n zero) (negative n)))

Theorem: The conjunction of negative-pred-split and negative-pred-split-conv.

(negative (pred zero))

Theorem: The predecessor of zero is negative.

(elem (pred n) nat)

Definition: The integer n is strictly positive.

(==> (positive n) (elem n nat))

Theorem: A positive natural number is (obiously) a natural number

(forall-in [x nat] (==> (not (= x zero)) (positive x)))

Theorem: Any non-zero natural number is positive.

(not (positive zero))

Theorem:

(==> (elem n nat) (positive (succ n)))

Theorem: The successor of a natural number is positive.

(==> (positive (succ n)) (elem n nat))

Theorem: A successor of a positive natural number is (obiously) a natural number

(<=> (positive (succ n)) (elem n nat))

Theorem: A positive number is a natural number.

(==> (positive (succ n)) (or (= n zero) (positive n)))

Theorem: A positive successor can split.

(==> (or (= n zero) (positive n)) (positive (succ n)))

Theorem: The converse of positive-succ-split.

(<=> (positive (succ n)) (or (= n zero) (positive n)))

Theorem: The conjunction of positive-succ-split and positive-succ-split-conv.

(==> (positive n) (positive (succ n)))

Theorem: The successor of a positive is positive.

(==> (or (= n zero) (positive n)) (elem n nat))

Theorem: A positive or null number is … natural

(not (= one zero))

Theorem: A direct consequence of nat-zero-is-not-succ.