data.pnat.basic

# The positive natural numbers

This file defines the type ℕ+ or pnat, the subtype of natural numbers that are positive.

def pnat  :
Type

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Equations
@[instance]
def coe_pnat_nat  :

Equations
@[instance]

Equations
def pnat.nat_pred (i : ℕ+) :

Predecessor of a ℕ+, as a ℕ.

Equations
def nat.to_pnat (n : ) (h : 0 < n . "exact_dec_trivial") :

Convert a natural number to a positive natural number. The positivity assumption is inferred by dec_trivial.

Equations
def nat.succ_pnat (n : ) :

Write a successor as an element of ℕ+.

Equations
@[simp]
theorem nat.succ_pnat_coe (n : ) :

theorem nat.succ_pnat_inj {n m : } :
n = m

def nat.to_pnat' (n : ) :

Convert a natural number to a pnat. n+1 is mapped to itself, and 0 becomes 1.

Equations
@[simp]
theorem nat.to_pnat'_coe (n : ) :
(n.to_pnat') = ite (0 < n) n 1

@[instance]

We now define a long list of structures on ℕ+ induced by similar structures on ℕ. Most of these behave in a completely obvious way, but there are a few things to be said about subtraction, division and powers.

Equations
@[instance]

Equations
@[simp]
theorem pnat.mk_le_mk (n k : ) (hn : 0 < n) (hk : 0 < k) :
n, hn⟩ k, hk⟩ n k

@[simp]
theorem pnat.mk_lt_mk (n k : ) (hn : 0 < n) (hk : 0 < k) :
n, hn⟩ < k, hk⟩ n < k

@[simp]
theorem pnat.coe_le_coe (n k : ℕ+) :
n k n k

@[simp]
theorem pnat.coe_lt_coe (n k : ℕ+) :
n < k n < k

@[simp]
theorem pnat.pos (n : ℕ+) :
0 < n

theorem pnat.eq {m n : ℕ+} :
m = nm = n

@[simp]
theorem pnat.coe_inj {m n : ℕ+} :
m = n m = n

@[simp]
theorem pnat.mk_coe (n : ) (h : 0 < n) :
n, h⟩ = n

@[instance]

Equations
@[simp]
theorem pnat.add_coe (m n : ℕ+) :
(m + n) = m + n

@[instance]

@[instance]

Equations
@[instance]

Equations
@[simp]
theorem pnat.ne_zero (n : ℕ+) :
n 0

theorem pnat.to_pnat'_coe {n : } :
0 < n(n.to_pnat') = n

@[simp]
theorem pnat.coe_to_pnat' (n : ℕ+) :

@[instance]

Equations
theorem pnat.lt_add_one_iff {a b : ℕ+} :
a < b + 1 a b

theorem pnat.add_one_le_iff {a b : ℕ+} :
a + 1 b a < b

@[simp]
theorem pnat.one_le (n : ℕ+) :
1 n

@[instance]

Equations
@[simp]
theorem pnat.bot_eq_zero  :
= 1

@[instance]

Equations
@[simp]
theorem pnat.mk_one {h : 0 < 1} :
1, h⟩ = 1

@[simp]
theorem pnat.mk_bit0 (n : ) {h : 0 < bit0 n} :
bit0 n, h⟩ = bit0 n, _⟩

@[simp]
theorem pnat.mk_bit1 (n : ) {h : 0 < bit1 n} {k : 0 < n} :
bit1 n, h⟩ = bit1 n, k⟩

@[simp]
theorem pnat.bit0_le_bit0 (n m : ℕ+) :

@[simp]
theorem pnat.bit0_le_bit1 (n m : ℕ+) :

@[simp]
theorem pnat.bit1_le_bit0 (n m : ℕ+) :

@[simp]
theorem pnat.bit1_le_bit1 (n m : ℕ+) :

@[simp]
theorem pnat.one_coe  :
1 = 1

@[simp]
theorem pnat.mul_coe (m n : ℕ+) :
m * n = (m) * n

@[instance]

@[simp]
theorem pnat.coe_eq_one_iff {m : ℕ+} :
m = 1 m = 1

@[simp]
theorem pnat.coe_bit0 (a : ℕ+) :
(bit0 a) =

@[simp]
theorem pnat.coe_bit1 (a : ℕ+) :
(bit1 a) =

@[simp]
theorem pnat.pow_coe (m : ℕ+) (n : ) :
(m ^ n) = m ^ n

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Subtraction a - b is defined in the obvious way when a > b, and by a - b = 1 if a ≤ b.

Equations
theorem pnat.sub_coe (a b : ℕ+) :
(a - b) = ite (b < a) (a - b) 1

theorem pnat.add_sub_of_lt {a b : ℕ+} :
a < ba + (b - a) = b

@[instance]

Equations
theorem pnat.strong_induction_on {p : ℕ+ → Prop} (n : ℕ+) (h : ∀ (k : ℕ+), (∀ (m : ℕ+), m < kp m)p k) :
p n

Strong induction on pnat.

theorem pnat.exists_eq_succ_of_ne_one {n : ℕ+} (h1 : n 1) :
∃ (k : ℕ+), n = k + 1

If (n : pnat) is different from 1, then it is the successor of some (k : pnat).

theorem pnat.case_strong_induction_on {p : ℕ+ → Prop} (a : ℕ+) (hz : p 1) (hi : ∀ (n : ℕ+), (∀ (m : ℕ+), m np m)p (n + 1)) :
p a

def pnat.mod_div_aux  :
ℕ+

We define m % k and m / k in the same way as for ℕ except that when m = n * k we take m % k = k and m / k = n - 1. This ensures that m % k is always positive and m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

Equations
theorem pnat.mod_div_aux_spec (k : ℕ+) (r q : ) (h : ¬(r = 0 q = 0)) :
((k.mod_div_aux r q).fst) + (k) * (k.mod_div_aux r q).snd = r + (k) * q

def pnat.mod_div (m k : ℕ+) :

mod_div m k = (m % k, m / k). We define m % k and m / k in the same way as for ℕ except that when m = n * k we take m % k = k and m / k = n - 1. This ensures that m % k is always positive and m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

Equations
def pnat.mod (m k : ℕ+) :

We define m % k in the same way as for ℕ except that when m = n * k we take m % k = k This ensures that m % k is always positive.

Equations
def pnat.div (m k : ℕ+) :

We define m / k in the same way as for ℕ except that when m = n * k we take m / k = n - 1. This ensures that m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

Equations
theorem pnat.mod_add_div (m k : ℕ+) :
m = (m.mod k) + (k) * m.div k

theorem pnat.mod_coe (m k : ℕ+) :
(m.mod k) = ite (m % k = 0) k (m % k)

theorem pnat.div_coe (m k : ℕ+) :
m.div k = ite (m % k = 0) (m / k).pred (m / k)

theorem pnat.mod_le (m k : ℕ+) :
m.mod k m m.mod k k

theorem pnat.dvd_iff {k m : ℕ+} :
k m k m

theorem pnat.dvd_iff' {k m : ℕ+} :
k m m.mod k = k

theorem pnat.le_of_dvd {m n : ℕ+} :
m nm n

def pnat.div_exact (m k : ℕ+) :

If h : k | m, then k * (div_exact m k) = m. Note that this is not equal to m / k.

Equations
theorem pnat.mul_div_exact {m k : ℕ+} (h : k m) :
k * m.div_exact k = m

theorem pnat.dvd_antisymm {m n : ℕ+} :
m nn mm = n

theorem pnat.dvd_one_iff (n : ℕ+) :
n 1 n = 1

theorem pnat.pos_of_div_pos {n : ℕ+} {a : } (h : a n) :
0 < a