# The positive natural numbers #

This file contains the definitions, and basic results. Most algebraic facts are deferred to Data.PNat.Basic, as they need more imports.

def PNat :

ℕ+ 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
Instances For

ℕ+ 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
Instances For
instance instOnePNat :
Equations
def PNat.val :
ℕ+

The underlying natural number

Equations
Instances For
instance coePNatNat :
Equations
instance instReprPNat :
Equations
Equations
• = { ofNat := { val := n + 1, property := } }
@[simp]
theorem PNat.mk_coe (n : ) (h : 0 < n) :
{ val := n, property := h } = n
def PNat.natPred (i : ℕ+) :

Predecessor of a ℕ+, as a ℕ.

Equations
• = i - 1
Instances For
@[simp]
theorem PNat.natPred_eq_pred {n : } (h : 0 < n) :
PNat.natPred { val := n, property := h } =
def Nat.toPNat (n : ) (h : autoParam (0 < n) _auto✝) :

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

Equations
• = { val := n, property := h }
Instances For
def Nat.succPNat (n : ) :

Write a successor as an element of ℕ+.

Equations
• = { val := , property := }
Instances For
@[simp]
theorem Nat.succPNat_coe (n : ) :
() =
@[simp]
theorem Nat.natPred_succPNat (n : ) :
@[simp]
theorem PNat.succPNat_natPred (n : ℕ+) :
def Nat.toPNat' (n : ) :

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

Equations
Instances For
@[simp]
theorem Nat.toPNat'_zero :
= 1
@[simp]
theorem Nat.toPNat'_coe (n : ) :
() = if 0 < n then n else 1
theorem PNat.mk_le_mk (n : ) (k : ) (hn : 0 < n) (hk : 0 < k) :
{ val := n, property := hn } { val := k, property := hk } n k

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.

theorem PNat.mk_lt_mk (n : ) (k : ) (hn : 0 < n) (hk : 0 < k) :
{ val := n, property := hn } < { val := k, property := 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.ne_zero (n : ℕ+) :
n 0
instance NeZero.pnat {a : ℕ+} :
NeZero a
Equations
• =
theorem PNat.toPNat'_coe {n : } :
0 < n() = n
@[simp]
theorem PNat.coe_toPNat' (n : ℕ+) :
= n
@[simp]
theorem PNat.one_le (n : ℕ+) :
1 n
@[simp]
theorem PNat.not_lt_one (n : ℕ+) :
¬n < 1
Equations
@[simp]
theorem PNat.mk_one {h : 0 < 1} :
{ val := 1, property := h } = 1
theorem PNat.one_coe :
1 = 1
@[simp]
theorem PNat.coe_eq_one_iff {m : ℕ+} :
m = 1 m = 1
def PNat.strongInductionOn {p : ℕ+Sort u_1} (n : ℕ+) :
((k : ℕ+) → ((m : ℕ+) → m < kp m)p k)p n

Strong induction on ℕ+.

Equations
• = x n fun (a : ℕ+) (x_1 : a < n) =>
Instances For
def PNat.modDivAux :
ℕ+

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
• PNat.modDivAux x✝¹ x✝ x = match x✝¹, x✝, x with | k, 0, q => (k, ) | x, , q => ({ val := r + 1, property := }, q)
Instances For
def PNat.modDiv (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
Instances For
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
Instances For
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
Instances For
theorem PNat.mod_coe (m : ℕ+) (k : ℕ+) :
(PNat.mod m k) = if m % k = 0 then k else m % k
theorem PNat.div_coe (m : ℕ+) (k : ℕ+) :
PNat.div m k = if m % k = 0 then Nat.pred (m / k) else m / k
def PNat.divExact (m : ℕ+) (k : ℕ+) :

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

Equations
Instances For
instance Nat.canLiftPNat :
CanLift ℕ+ PNat.val fun (n : ) => 0 < n
Equations
instance Int.canLiftPNat :
CanLift ℕ+ (fun (x : ℕ+) => x) fun (x : ) => 0 < x
Equations