# Documentation

Mathlib.Data.PNat.Basic

# The positive natural numbers #

This file develops the type ℕ+ or PNat, the subtype of natural numbers that are positive. It is defined in Data.PNat.Defs, but most of the development is deferred to here so that Data.PNat.Defs can have very few imports.

@[simp]
theorem PNat.one_add_natPred (n : ℕ+) :
= n
@[simp]
theorem PNat.natPred_add_one (n : ℕ+) :
= n
@[simp]
theorem PNat.natPred_lt_natPred {m : ℕ+} {n : ℕ+} :
m < n
@[simp]
theorem PNat.natPred_le_natPred {m : ℕ+} {n : ℕ+} :
m n
@[simp]
theorem PNat.natPred_inj {m : ℕ+} {n : ℕ+} :
m = n
@[simp]
theorem Nat.succPNat_lt_succPNat {m : } {n : } :
m < n
@[simp]
theorem Nat.succPNat_le_succPNat {m : } {n : } :
m n
@[simp]
theorem Nat.succPNat_inj {n : } {m : } :
n = m
@[simp]
theorem PNat.coe_inj {m : ℕ+} {n : ℕ+} :
m = n m = n

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.

@[simp]
theorem PNat.add_coe (m : ℕ+) (n : ℕ+) :
↑(m + n) = m + n

coe promoted to an AddHom, that is, a morphism which preserves addition.

Equations
CovariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
CovariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
ContravariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
ContravariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
@[simp]
@[simp]

An equivalence between ℕ+ and ℕ given by PNat.natPred and Nat.succPNat.

Equations
@[simp]
theorem OrderIso.pnatIsoNat_apply :
().toEmbedding = PNat.natPred

The order isomorphism between ℕ and ℕ+ given by succ.

Equations
@[simp]
theorem OrderIso.pnatIsoNat_symm_apply :
().toEmbedding = Nat.succPNat
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
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem PNat.bot_eq_one :
= 1
@[simp]
theorem PNat.mk_bit0 (n : ) {h : 0 < bit0 n} :
{ val := bit0 n, property := h } = bit0 { val := n, property := (_ : 0 < n) }
@[simp]
theorem PNat.mk_bit1 (n : ) {h : 0 < bit1 n} {k : 0 < n} :
{ val := bit1 n, property := h } = bit1 { val := n, property := k }
@[simp]
theorem PNat.bit0_le_bit0 (n : ℕ+) (m : ℕ+) :
bit0 n bit0 m bit0 n bit0 m
@[simp]
theorem PNat.bit0_le_bit1 (n : ℕ+) (m : ℕ+) :
bit0 n bit1 m bit0 n bit1 m
@[simp]
theorem PNat.bit1_le_bit0 (n : ℕ+) (m : ℕ+) :
bit1 n bit0 m bit1 n bit0 m
@[simp]
theorem PNat.bit1_le_bit1 (n : ℕ+) (m : ℕ+) :
bit1 n bit1 m bit1 n bit1 m
@[simp]
theorem PNat.mul_coe (m : ℕ+) (n : ℕ+) :
↑(m * n) = m * n

PNat.coe promoted to a MonoidHom.

Equations
@[simp]
theorem PNat.coe_coeMonoidHom :
= Coe.coe
@[simp]
theorem PNat.le_one_iff {n : ℕ+} :
n 1 n = 1
theorem PNat.lt_add_left (n : ℕ+) (m : ℕ+) :
n < m + n
theorem PNat.lt_add_right (n : ℕ+) (m : ℕ+) :
n < n + m
@[simp]
theorem PNat.coe_bit0 (a : ℕ+) :
↑(bit0 a) = bit0 a
@[simp]
theorem PNat.coe_bit1 (a : ℕ+) :
↑(bit1 a) = bit1 a
@[simp]
theorem PNat.pow_coe (m : ℕ+) (n : ) :
↑(Pow.pow m n) = m ^ n
instance PNat.instSubPNat :

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) = if b < a then a - b else 1
theorem PNat.add_sub_of_lt {a : ℕ+} {b : ℕ+} :
a < ba + (b - a) = b
theorem PNat.exists_eq_succ_of_ne_one {n : ℕ+} :
n 1k, n = k + 1

If n : ℕ+ is different from 1, then it is the successor of some k : ℕ+.

def PNat.caseStrongInductionOn {p : ℕ+Sort u_1} (a : ℕ+) (hz : p 1) (hi : (n : ℕ+) → ((m : ℕ+) → m np m) → p (n + 1)) :
p a

Strong induction on ℕ+, with n = 1 treated separately.

Equations
• One or more equations did not get rendered due to their size.
def PNat.recOn (n : ℕ+) {p : ℕ+Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p np (n + 1)) :
p n

An induction principle for ℕ+: it takes values in Sort*, so it applies also to Types, not only to Prop.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem PNat.recOn_one {p : ℕ+Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p np (n + 1)) :
PNat.recOn 1 p1 hp = p1
@[simp]
theorem PNat.recOn_succ (n : ℕ+) {p : ℕ+Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p np (n + 1)) :
PNat.recOn (n + 1) p1 hp = hp n (PNat.recOn n p1 hp)
theorem PNat.modDivAux_spec (k : ℕ+) (r : ) (q : ) :
¬(r = 0 q = 0)().fst + k * ().snd = r + k * q
theorem PNat.mod_add_div (m : ℕ+) (k : ℕ+) :
↑(PNat.mod m k) + k * PNat.div m k = m
theorem PNat.div_add_mod (m : ℕ+) (k : ℕ+) :
k * PNat.div m k + ↑(PNat.mod m k) = m
theorem PNat.mod_add_div' (m : ℕ+) (k : ℕ+) :
↑(PNat.mod m k) + PNat.div m k * k = m
theorem PNat.div_add_mod' (m : ℕ+) (k : ℕ+) :
PNat.div m k * k + ↑(PNat.mod m k) = m
theorem PNat.mod_le (m : ℕ+) (k : ℕ+) :
theorem PNat.dvd_iff {k : ℕ+} {m : ℕ+} :
k m k m
theorem PNat.dvd_iff' {k : ℕ+} {m : ℕ+} :
k m PNat.mod m k = k
theorem PNat.le_of_dvd {m : ℕ+} {n : ℕ+} :
m nm n
theorem PNat.mul_div_exact {m : ℕ+} {k : ℕ+} (h : k m) :
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