# Maths in Lean : the natural numbers

The natural numbers begin with zero as is standard in computer
science. You can call them `nat` or `ℕ` (you get the latter
symbol by typing `\N` in VS Code).

The naturals are what is called an inductive type, with two
constructors. The first is `nat.zero`, usually written `0` or `(0:ℕ)` in
practice, which is zero. The other constructor is `nat.succ`, which
takes a natural as input and outputs the next one.

Addition and multiplication are defined by recursion on the second
variable and many proofs of basic stuff in the core library are by
induction on the second variable. The notations `+,-,*` are shorthand
for the functions `nat.add`, `nat.sub` and `nat.mul` and other notations
(≤, <, |) mean the usual things (get the "divides" symbol with `\|`.
The `%` symbol denotes modulus (remainder after division).

Here are some of core Lean's functions for working with `nat`.

```lean
open nat

example : nat.succ (nat.succ 4) = 6 := rfl

example : 4 - 3 = 1 := rfl

example : 5 - 6 = 0 := rfl -- these are naturals

example : 1 ≠ 0 := one_ne_zero

example : 7 * 4 = 28 := rfl

example (m n p : ℕ) : m + p = n + p → m = n := add_right_cancel

example (a b c : ℕ) : a * (b + c) = a * b + a * c := left_distrib a b c

example (m n : ℕ) : succ m ≤ succ n → m ≤ n := le_of_succ_le_succ

example (a b: ℕ) : a < b → ∀ n, 0 < n → a ^ n < b ^ n := pow_lt_pow_of_lt_left
```

In mathlib there are more basic functions on the naturals, for example
factorials, lowest common multiples, primes, square roots, and some
modular arithmetic.

```lean
import data.nat.dist -- distance function
import data.nat.gcd -- gcd
import data.nat.modeq -- modular arithmetic
import data.nat.prime -- prime number stuff
import data.nat.sqrt  -- square roots
import tactic.norm_num -- a tactic for fast computations

open nat

example : fact 4 = 24 := rfl -- factorial

example (a : ℕ) : fact a > 0 := fact_pos a

example : dist 6 4 = 2 := rfl -- distance function

example (a b : ℕ) : a ≠ b → dist a b > 0 := dist_pos_of_ne

example (a b : ℕ) : gcd a b ∣ a ∧ gcd a b ∣ b := gcd_dvd a b

example : lcm 6 4 = 12 := rfl

example (a b : ℕ) : lcm a b = lcm b a := lcm_comm a b
example (a b : ℕ) : gcd a b * lcm a b = a * b := gcd_mul_lcm a b

example (a b : ℕ) : (∀ k : ℕ, k > 1 → k ∣ a → ¬ (k ∣ b) ) → coprime a b := coprime_of_dvd

-- type the congruence symbol with \==

example : 5 ≡ 8 [MOD 3] := rfl

example (a b c d m : ℕ) : a ≡ b [MOD m] → c ≡ d [MOD m] → a * c ≡ b * d [MOD m] := modeq.modeq_mul

-- nat.sqrt is integer square root (it rounds down).

#eval sqrt 1000047
-- returns 1000

example (a : ℕ) : sqrt (a * a) = a := sqrt_eq a

example (a b : ℕ) : sqrt a < b ↔ a < b * b := sqrt_lt

-- nat.prime n returns whether n is prime or not.
-- We can prove 59 is prime if we first tell Lean that primality
-- is decidable. But it's slow because the algorithms are
-- not optimised for the kernel.

instance : decidable (prime 59) := decidable_prime_1 59
example : prime 59 := dec_trivial

-- (The default instance is `nat.decidable_prime`, which can't be
-- used by `dec_trivial`, because the kernel would need to unfold
-- irreducible proofs generated by well-founded recursion.)

-- The tactic `norm_num`, amongst other things, provides faster primality testing.

example : prime 104729 := by norm_num

example (p : ℕ) : prime p → p ≥ 2 := prime.two_le

example (p : ℕ) : prime p ↔ p ≥ 2 ∧ ∀ m, 2 ≤ m → m ≤ sqrt p → ¬ (m ∣ p) := prime_def_le_sqrt

example (p : ℕ) : prime p → (∀ m, coprime p m ∨ p ∣ m) := coprime_or_dvd_of_prime

example : ∀ n, ∃ p, p ≥ n ∧ prime p := exists_infinite_primes

-- min_fac returns the smallest prime factor of n (or junk if it doesn't have one)

example : min_fac 12 = 2 := rfl

-- `factors n` is the prime factorization of `n`, listed in increasing order.
-- This doesn't seem to reduce, and apparently there has not been
-- an attempt to get the kernel to evaluate it sensibly.
-- But we can evaluate it in the virtual machine using #eval .

#eval factors (2^32+1)
-- [641, 6700417]
```
