An example Rocq blueprint project

1 The naturals

In this chapter we give some basic definitions and lemmas about the natural numbers.

Definition 1
#

The set of naturals, denoted \(\mathbb {N}\), is the set of numbers \(\{ 0, 1, 2, \ldots \} \).

Lemma 2
#

Let \(n\) be a natural number. Then \(n = n + 0\).

Proof
Lemma 3
#

Let \(n\) and \(m\) be natural numbers. Then \((n + m) + 1 = n + (m + 1)\).

Proof
Lemma 4

Addition is commutative, i.e. \(n+m = m+n\) for all \(m, n\in \mathbb {N}\).

Proof
Lemma 5

Let \(n\) be a natural number. Then \(2*n = n + 2\).

Proof

The proof is trivial and left as an exercise to the reader.