mathlib3 documentation

data.nat.basic

Basic operations on the natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains:

instances on the natural numbers
some basic lemmas about natural numbers
extra recursors:
- le_rec_on, le_induction: recursion and induction principles starting at non-zero numbers
- decreasing_induction: recursion growing downwards
- le_rec_on', decreasing_induction': versions with slightly weaker assumptions
- strong_rec': recursion based on strong inequalities
decidability instances on predicates about the natural numbers

Many theorems that used to live in this file have been moved to data.nat.order, so that this file requires fewer imports. For each section here there is a corresponding section in that file with additional results. It may be possible to move some of these results here, by tweaking their proofs.

instances #

@[protected, instance]

def nat.nontrivial :

@[protected, instance]

def nat.comm_semiring :

comm_semiring ℕ

Equations

nat.comm_semiring = {add := nat.add, add_assoc := nat.add_assoc, zero := 0, zero_add := nat.zero_add, add_zero := nat.add_zero, nsmul := λ (m n : ℕ), m * n, nsmul_zero' := nat.zero_mul, nsmul_succ' := nat.comm_semiring._proof_1, add_comm := nat.add_comm, mul := nat.mul, left_distrib := nat.left_distrib, right_distrib := nat.right_distrib, zero_mul := nat.zero_mul, mul_zero := nat.mul_zero, mul_assoc := nat.mul_assoc, one := 1, one_mul := nat.one_mul, mul_one := nat.mul_one, nat_cast := λ (n : ℕ), n, nat_cast_zero := nat.comm_semiring._proof_2, nat_cast_succ := nat.comm_semiring._proof_3, npow := semiring.npow._default 1 nat.mul nat.one_mul nat.mul_one, npow_zero' := nat.comm_semiring._proof_4, npow_succ' := nat.comm_semiring._proof_5, mul_comm := nat.mul_comm}

Extra instances to short-circuit type class resolution and ensure computability

@[protected, instance]

def nat.add_comm_monoid :

add_comm_monoid ℕ

Equations

nat.add_comm_monoid = infer_instance

@[protected, instance]

def nat.add_monoid :

Equations

nat.add_monoid = infer_instance

@[protected, instance]

def nat.monoid :

Equations

nat.monoid = infer_instance

@[protected, instance]

def nat.comm_monoid :

comm_monoid ℕ

Equations

nat.comm_monoid = infer_instance

@[protected, instance]

def nat.comm_semigroup :

comm_semigroup ℕ

Equations

nat.comm_semigroup = infer_instance

@[protected, instance]

def nat.semigroup :

Equations

nat.semigroup = infer_instance

@[protected, instance]

def nat.add_comm_semigroup :

add_comm_semigroup ℕ

Equations

nat.add_comm_semigroup = infer_instance

@[protected, instance]

def nat.add_semigroup :

add_semigroup ℕ

Equations

nat.add_semigroup = infer_instance

@[protected, instance]

def nat.distrib :

Equations

nat.distrib = infer_instance

@[protected, instance]

def nat.semiring :

Equations

nat.semiring = infer_instance

@[protected]

theorem nat.nsmul_eq_mul (m n : ℕ) :

m • n = m * n

@[protected, instance]

def nat.cancel_comm_monoid_with_zero :

cancel_comm_monoid_with_zero ℕ

Equations

nat.cancel_comm_monoid_with_zero = {mul := comm_semiring.mul nat.comm_semiring, mul_assoc := _, one := comm_semiring.one nat.comm_semiring, one_mul := _, mul_one := _, npow := comm_semiring.npow nat.comm_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := comm_semiring.zero nat.comm_semiring, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := nat.cancel_comm_monoid_with_zero._proof_1}

Recursion and `forall`/`exists` #

@[simp]

theorem nat.and_forall_succ {p : ℕ → Prop} :

(p 0 ∧ ∀ (n : ℕ), p (n + 1)) ↔ ∀ (n : ℕ), p n

@[simp]

theorem nat.or_exists_succ {p : ℕ → Prop} :

(p 0 ∨ ∃ (n : ℕ), p (n + 1)) ↔ ∃ (n : ℕ), p n

`succ` #

theorem has_lt.lt.nat_succ_le {n m : ℕ} (h : n < m) :

theorem nat.succ_eq_one_add (n : ℕ) :

n.succ = 1 + n

theorem nat.eq_of_lt_succ_of_not_lt {a b : ℕ} (h1 : a < b + 1) (h2 : ¬a < b) :

a = b

theorem nat.eq_of_le_of_lt_succ {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n + 1) :

m = n

theorem nat.one_add (n : ℕ) :

1 + n = n.succ

@[simp]

theorem nat.succ_pos' {n : ℕ} :

0 < n.succ

theorem nat.succ_inj' {n m : ℕ} :

n.succ = m.succ ↔ n = m

theorem nat.succ_injective :

function.injective nat.succ

theorem nat.succ_ne_succ {n m : ℕ} :

n.succ ≠ m.succ ↔ n ≠ m

@[simp]

theorem nat.succ_succ_ne_one (n : ℕ) :

n.succ.succ ≠ 1

@[simp]

theorem nat.one_lt_succ_succ (n : ℕ) :

1 < n.succ.succ

theorem nat.succ_le_succ_iff {m n : ℕ} :

m.succ ≤ n.succ ↔ m ≤ n

theorem nat.max_succ_succ {m n : ℕ} :

linear_order.max m.succ n.succ = (linear_order.max m n).succ

theorem nat.not_succ_lt_self {n : ℕ} :

theorem nat.lt_succ_iff {m n : ℕ} :

m < n.succ ↔ m ≤ n

theorem nat.succ_le_iff {m n : ℕ} :

m.succ ≤ n ↔ m < n

theorem nat.lt_iff_add_one_le {m n : ℕ} :

m < n ↔ m + 1 ≤ n

theorem nat.lt_add_one_iff {a b : ℕ} :

a < b + 1 ↔ a ≤ b

theorem nat.lt_one_add_iff {a b : ℕ} :

a < 1 + b ↔ a ≤ b

theorem nat.add_one_le_iff {a b : ℕ} :

a + 1 ≤ b ↔ a < b

theorem nat.one_add_le_iff {a b : ℕ} :

1 + a ≤ b ↔ a < b

theorem nat.of_le_succ {n m : ℕ} (H : n ≤ m.succ) :

n ≤ m ∨ n = m.succ

theorem nat.succ_lt_succ_iff {m n : ℕ} :

m.succ < n.succ ↔ m < n

theorem nat.div_le_iff_le_mul_add_pred {m n k : ℕ} (n0 : 0 < n) :

m / n ≤ k ↔ m ≤ n * k + (n - 1)

theorem nat.two_lt_of_ne {n : ℕ} :

n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n

theorem nat.forall_lt_succ {P : ℕ → Prop} {n : ℕ} :

(∀ (m : ℕ), m < n + 1 → P m) ↔ (∀ (m : ℕ), m < n → P m) ∧ P n

theorem nat.exists_lt_succ {P : ℕ → Prop} {n : ℕ} :

(∃ (m : ℕ) (H : m < n + 1), P m) ↔ (∃ (m : ℕ) (H : m < n), P m) ∨ P n

`add` #

@[simp]

theorem nat.add_def {a b : ℕ} :

a.add b = a + b

@[simp]

theorem nat.mul_def {a b : ℕ} :

a.mul b = a * b

theorem nat.exists_eq_add_of_le {m n : ℕ} (h : m ≤ n) :

∃ (k : ℕ), n = m + k

theorem nat.exists_eq_add_of_le' {m n : ℕ} (h : m ≤ n) :

∃ (k : ℕ), n = k + m

theorem nat.exists_eq_add_of_lt {m n : ℕ} (h : m < n) :

∃ (k : ℕ), n = m + k + 1

`pred` #

@[simp]

theorem nat.add_succ_sub_one (n m : ℕ) :

n + m.succ - 1 = n + m

@[simp]

theorem nat.succ_add_sub_one (n m : ℕ) :

n.succ + m - 1 = n + m

theorem nat.pred_eq_sub_one (n : ℕ) :

n.pred = n - 1

theorem nat.pred_eq_of_eq_succ {m n : ℕ} (H : m = n.succ) :

m.pred = n

@[simp]

theorem nat.pred_eq_succ_iff {n m : ℕ} :

n.pred = m.succ ↔ n = m + 2

theorem nat.pred_sub (n m : ℕ) :

n.pred - m = (n - m).pred

theorem nat.le_pred_of_lt {n m : ℕ} (h : m < n) :

m ≤ n - 1

theorem nat.le_of_pred_lt {m n : ℕ} :

m.pred < n → m ≤ n

@[simp]

theorem nat.pred_one_add (n : ℕ) :

(1 + n).pred = n

This ensures that simp succeeds on pred (n + 1) = n.

`mul` #

theorem nat.two_mul_ne_two_mul_add_one {n m : ℕ} :

2 * n ≠ 2 * m + 1

theorem nat.mul_ne_mul_left {a b c : ℕ} (ha : 0 < a) :

b * a ≠ c * a ↔ b ≠ c

theorem nat.mul_ne_mul_right {a b c : ℕ} (ha : 0 < a) :

a * b ≠ a * c ↔ b ≠ c

theorem nat.mul_right_eq_self_iff {a b : ℕ} (ha : 0 < a) :

a * b = a ↔ b = 1

theorem nat.mul_left_eq_self_iff {a b : ℕ} (hb : 0 < b) :

a * b = b ↔ a = 1

theorem nat.lt_succ_iff_lt_or_eq {n i : ℕ} :

n < i.succ ↔ n < i ∨ n = i

Recursion and induction principles #

This section is here due to dependencies -- the lemmas here require some of the lemmas proved above, and some of the results in later sections depend on the definitions in this section.

@[simp]

theorem nat.rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : Π (n : ℕ), C n → C (n + 1)) :

nat.rec h0 h 0 = h0

@[simp]

theorem nat.rec_add_one {C : ℕ → Sort u} (h0 : C 0) (h : Π (n : ℕ), C n → C (n + 1)) (n : ℕ) :

nat.rec h0 h (n + 1) = h n (nat.rec h0 h n)

def nat.le_rec_on {C : ℕ → Sort u} {n m : ℕ} :

n ≤ m → (Π {k : ℕ}, C k → C (k + 1)) → C n → C m

Recursion starting at a non-zero number: given a map C k → C (k+1) for each k, there is a map from C n to each C m, n ≤ m. For a version where the assumption is only made when k ≥ n, see le_rec_on'.

Equations

nat.le_rec_on H next x = _.by_cases (λ (h : n ≤ m), next (nat.le_rec_on h next x)) (λ (h : n = m + 1), h.rec_on x)
nat.le_rec_on H next x = _.rec_on x

theorem nat.le_rec_on_self {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :

nat.le_rec_on h next x = x

theorem nat.le_rec_on_succ {C : ℕ → Sort u} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :

nat.le_rec_on h2 next x = next (nat.le_rec_on h1 next x)

theorem nat.le_rec_on_succ' {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n + 1} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :

nat.le_rec_on h next x = next x

theorem nat.le_rec_on_trans {C : ℕ → Sort u} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :

nat.le_rec_on _ next x = nat.le_rec_on hmk next (nat.le_rec_on hnm next x)

theorem nat.le_rec_on_succ_left {C : ℕ → Sort u} {n m : ℕ} (h1 : n ≤ m) (h2 : n + 1 ≤ m) {next : Π ⦃k : ℕ⦄, C k → C (k + 1)} (x : C n) :

nat.le_rec_on h2 next (next x) = nat.le_rec_on h1 next x

theorem nat.le_rec_on_injective {C : ℕ → Sort u} {n m : ℕ} (hnm : n ≤ m) (next : Π (n : ℕ), C n → C (n + 1)) (Hnext : ∀ (n : ℕ), function.injective (next n)) :

function.injective (nat.le_rec_on hnm next)

theorem nat.le_rec_on_surjective {C : ℕ → Sort u} {n m : ℕ} (hnm : n ≤ m) (next : Π (n : ℕ), C n → C (n + 1)) (Hnext : ∀ (n : ℕ), function.surjective (next n)) :

function.surjective (nat.le_rec_on hnm next)

@[protected]

def nat.strong_rec' {p : ℕ → Sort u} (H : Π (n : ℕ), (Π (m : ℕ), m < n → p m) → p n) (n : ℕ) :

p n

Recursion principle based on <.

Equations

nat.strong_rec' H n = H n (λ (m : ℕ) (hm : m < n), nat.strong_rec' H m)

def nat.strong_rec_on' {P : ℕ → Sort u_1} (n : ℕ) (h : Π (n : ℕ), (Π (m : ℕ), m < n → P m) → P n) :

P n

Recursion principle based on < applied to some natural number.

Equations

n.strong_rec_on' h = nat.strong_rec' h n

theorem nat.strong_rec_on_beta' {P : ℕ → Sort u_1} {h : Π (n : ℕ), (Π (m : ℕ), m < n → P m) → P n} {n : ℕ} :

n.strong_rec_on' h = h n (λ (m : ℕ) (hmn : m < n), m.strong_rec_on' h)

theorem nat.le_induction {P : ℕ → Prop} {m : ℕ} (h0 : P m) (h1 : ∀ (n : ℕ), m ≤ n → P n → P (n + 1)) (n : ℕ) :

m ≤ n → P n

Induction principle starting at a non-zero number. For maps to a Sort* see le_rec_on.

def nat.decreasing_induction {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} (mn : m ≤ n) (hP : P n) :

P m

Decreasing induction: if P (k+1) implies P k, then P n implies P m for all m ≤ n. Also works for functions to Sort*. For a version assuming only the assumption for k < n, see decreasing_induction'.

Equations

nat.decreasing_induction h mn hP = nat.le_rec_on mn (λ (k : ℕ) (ih : P k → P m) (hsk : P (k + 1)), ih (h k hsk)) (λ (h : P m), h) hP

@[simp]

theorem nat.decreasing_induction_self {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {n : ℕ} (nn : n ≤ n) (hP : P n) :

nat.decreasing_induction h nn hP = hP

theorem nat.decreasing_induction_succ {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} (mn : m ≤ n) (msn : m ≤ n + 1) (hP : P (n + 1)) :

nat.decreasing_induction h msn hP = nat.decreasing_induction h mn (h n hP)

@[simp]

theorem nat.decreasing_induction_succ' {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m : ℕ} (msm : m ≤ m + 1) (hP : P (m + 1)) :

nat.decreasing_induction h msm hP = h m hP

theorem nat.decreasing_induction_trans {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n k : ℕ} (mn : m ≤ n) (nk : n ≤ k) (hP : P k) :

nat.decreasing_induction h _ hP = nat.decreasing_induction h mn (nat.decreasing_induction h nk hP)

theorem nat.decreasing_induction_succ_left {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} (smn : m + 1 ≤ n) (mn : m ≤ n) (hP : P n) :

nat.decreasing_induction h mn hP = h m (nat.decreasing_induction h smn hP)

def nat.strong_sub_recursion {P : ℕ → ℕ → Sort u_1} (H : Π (a b : ℕ), (Π (x y : ℕ), x < a → y < b → P x y) → P a b) (n m : ℕ) :

P n m

Given P : ℕ → ℕ → Sort*, if for all a b : ℕ we can extend P from the rectangle strictly below (a,b) to P a b, then we have P n m for all n m : ℕ. Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

Equations

nat.strong_sub_recursion H n m = H n m (λ (x y : ℕ) (hx : x < n) (hy : y < m), nat.strong_sub_recursion H x y)

def nat.pincer_recursion {P : ℕ → ℕ → Sort u_1} (Ha0 : Π (a : ℕ), P a 0) (H0b : Π (b : ℕ), P 0 b) (H : Π (x y : ℕ), P x y.succ → P x.succ y → P x.succ y.succ) (n m : ℕ) :

P n m

Given P : ℕ → ℕ → Sort*, if we have P i 0 and P 0 i for all i : ℕ, and for any x y : ℕ we can extend P from (x,y+1) and (x+1,y) to (x+1,y+1) then we have P n m for all n m : ℕ. Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

Equations

nat.pincer_recursion Ha0 H0b H a.succ b.succ = H a b (nat.pincer_recursion Ha0 H0b H a b.succ) (nat.pincer_recursion Ha0 H0b H a.succ b)
nat.pincer_recursion Ha0 H0b H n.succ 0 = Ha0 n.succ
nat.pincer_recursion Ha0 H0b H 0 n.succ = H0b n.succ
nat.pincer_recursion Ha0 H0b H 0 0 = Ha0 0

def nat.le_rec_on' {C : ℕ → Sort u_1} {n m : ℕ} :

n ≤ m → (Π ⦃k : ℕ⦄, n ≤ k → C k → C (k + 1)) → C n → C m

Recursion starting at a non-zero number: given a map C k → C (k+1) for each k ≥ n, there is a map from C n to each C m, n ≤ m.

Equations

nat.le_rec_on' H next x = _.by_cases (λ (h : n ≤ m), next h (nat.le_rec_on' h next x)) (λ (h : n = m + 1), h.rec_on x)
nat.le_rec_on' H next x = _.rec_on x

def nat.decreasing_induction' {P : ℕ → Sort u_1} {m n : ℕ} (h : Π (k : ℕ), k < n → m ≤ k → P (k + 1) → P k) (mn : m ≤ n) (hP : P n) :

P m

Decreasing induction: if P (k+1) implies P k for all m ≤ k < n, then P n implies P m. Also works for functions to Sort*. Weakens the assumptions of decreasing_induction.

Equations

nat.decreasing_induction' h mn hP = nat.le_rec_on' mn (λ (n : ℕ) (mn : m ≤ n) (ih : (Π (k : ℕ), k < n → m ≤ k → P (k + 1) → P k) → P n → P m) (h : Π (k : ℕ), k < n + 1 → m ≤ k → P (k + 1) → P k) (hP : P (n + 1)), ih (λ (k : ℕ) (hk : k < n), h k _) (h n _ mn hP)) (λ (h : Π (k : ℕ), k < m → m ≤ k → P (k + 1) → P k) (hP : P m), hP) h hP

`div` #

theorem nat.div_lt_self' (n b : ℕ) :

(n + 1) / (b + 2) < n + 1

A version of nat.div_lt_self using successors, rather than additional hypotheses.

theorem nat.le_div_iff_mul_le' {x y k : ℕ} (k0 : 0 < k) :

x ≤ y / k ↔ x * k ≤ y

theorem nat.div_lt_iff_lt_mul' {x y k : ℕ} (k0 : 0 < k) :

x / k < y ↔ x < y * k

theorem nat.one_le_div_iff {a b : ℕ} (hb : 0 < b) :

1 ≤ a / b ↔ b ≤ a

theorem nat.div_lt_one_iff {a b : ℕ} (hb : 0 < b) :

a / b < 1 ↔ a < b

@[protected]

theorem nat.div_le_div_right {n m : ℕ} (h : n ≤ m) {k : ℕ} :

n / k ≤ m / k

theorem nat.lt_of_div_lt_div {m n k : ℕ} :

m / k < n / k → m < n

@[protected]

theorem nat.div_pos {a b : ℕ} (hba : b ≤ a) (hb : 0 < b) :

0 < a / b

theorem nat.lt_mul_of_div_lt {a b c : ℕ} (h : a / c < b) (w : 0 < c) :

a < b * c

theorem nat.mul_div_le_mul_div_assoc (a b c : ℕ) :

a * (b / c) ≤ a * b / c

@[protected]

theorem nat.eq_mul_of_div_eq_right {a b c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) :

a = b * c

@[protected]

theorem nat.div_eq_iff_eq_mul_right {a b c : ℕ} (H : 0 < b) (H' : b ∣ a) :

a / b = c ↔ a = b * c

@[protected]

theorem nat.div_eq_iff_eq_mul_left {a b c : ℕ} (H : 0 < b) (H' : b ∣ a) :

a / b = c ↔ a = c * b

@[protected]

theorem nat.eq_mul_of_div_eq_left {a b c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) :

a = c * b

@[protected]

theorem nat.mul_div_cancel_left' {a b : ℕ} (Hd : a ∣ b) :

a * (b / a) = b

@[protected]

theorem nat.mul_div_mul_left (a b : ℕ) {c : ℕ} (hc : 0 < c) :

c * a / (c * b) = a / b

Alias of nat.mul_div_mul

@[protected]

theorem nat.mul_div_mul_right (a b : ℕ) {c : ℕ} (hc : 0 < c) :

a * c / (b * c) = a / b

theorem nat.lt_div_mul_add {a b : ℕ} (hb : 0 < b) :

a < a / b * b + b

@[protected, simp]

theorem nat.div_left_inj {a b d : ℕ} (hda : d ∣ a) (hdb : d ∣ b) :

a / d = b / d ↔ a = b

`mod`, `dvd` #

theorem nat.mod_eq_iff_lt {a b : ℕ} (h : b ≠ 0) :

a % b = a ↔ a < b

@[simp]

theorem nat.mod_succ_eq_iff_lt {a b : ℕ} :

a % b.succ = a ↔ a < b.succ

theorem nat.div_add_mod (m k : ℕ) :

k * (m / k) + m % k = m

theorem nat.mod_add_div' (m k : ℕ) :

m % k + m / k * k = m

theorem nat.div_add_mod' (m k : ℕ) :

m / k * k + m % k = m

@[protected]

theorem nat.div_mod_unique {n k m d : ℕ} (h : 0 < k) :

n / k = d ∧ n % k = m ↔ m + k * d = n ∧ m < k

See also nat.div_mod_equiv for a similar statement as an equiv.

@[protected]

theorem nat.dvd_add_left {k m n : ℕ} (h : k ∣ n) :

k ∣ m + n ↔ k ∣ m

@[protected]

theorem nat.dvd_add_right {k m n : ℕ} (h : k ∣ m) :

k ∣ m + n ↔ k ∣ n

@[protected]

theorem nat.mul_dvd_mul_iff_left {a b c : ℕ} (ha : 0 < a) :

a * b ∣ a * c ↔ b ∣ c

@[protected]

theorem nat.mul_dvd_mul_iff_right {a b c : ℕ} (hc : 0 < c) :

a * c ∣ b * c ↔ a ∣ b

@[simp]

theorem nat.mod_mod_of_dvd (n : ℕ) {m k : ℕ} (h : m ∣ k) :

n % k % m = n % m

@[simp]

theorem nat.mod_mod (a n : ℕ) :

a % n % n = a % n

@[simp]

theorem nat.mod_add_mod (m n k : ℕ) :

(m % n + k) % n = (m + k) % n

@[simp]

theorem nat.add_mod_mod (m n k : ℕ) :

(m + n % k) % k = (m + n) % k

theorem nat.add_mod (a b n : ℕ) :

(a + b) % n = (a % n + b % n) % n

theorem nat.add_mod_eq_add_mod_right {m n k : ℕ} (i : ℕ) (H : m % n = k % n) :

(m + i) % n = (k + i) % n

theorem nat.add_mod_eq_add_mod_left {m n k : ℕ} (i : ℕ) (H : m % n = k % n) :

(i + m) % n = (i + k) % n

theorem nat.mul_mod (a b n : ℕ) :

a * b % n = a % n * (b % n) % n

theorem nat.mul_dvd_of_dvd_div {a b c : ℕ} (hab : c ∣ b) (h : a ∣ b / c) :

c * a ∣ b

theorem nat.eq_of_dvd_of_div_eq_one {a b : ℕ} (w : a ∣ b) (h : b / a = 1) :

a = b

theorem nat.eq_zero_of_dvd_of_div_eq_zero {a b : ℕ} (w : a ∣ b) (h : b / a = 0) :

b = 0

theorem nat.div_le_div_left {a b c : ℕ} (h₁ : c ≤ b) (h₂ : 0 < c) :

a / b ≤ a / c

theorem nat.lt_iff_le_pred {m n : ℕ} :

0 < n → (m < n ↔ m ≤ n - 1)

theorem nat.mul_div_le (m n : ℕ) :

n * (m / n) ≤ m

theorem nat.lt_mul_div_succ (m : ℕ) {n : ℕ} (n0 : 0 < n) :

m < n * (m / n + 1)

theorem nat.mul_add_mod (a b c : ℕ) :

(a * b + c) % b = c % b

theorem nat.mul_add_mod_of_lt {a b c : ℕ} (h : c < b) :

(a * b + c) % b = c

theorem nat.pred_eq_self_iff {n : ℕ} :

n.pred = n ↔ n = 0

`find` #

theorem nat.find_eq_iff {m : ℕ} {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :

nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n

@[simp]

theorem nat.find_lt_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :

nat.find h < n ↔ ∃ (m : ℕ) (H : m < n), p m

@[simp]

theorem nat.find_le_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :

nat.find h ≤ n ↔ ∃ (m : ℕ) (H : m ≤ n), p m

@[simp]

theorem nat.le_find_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :

n ≤ nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m

@[simp]

theorem nat.lt_find_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :

n < nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m

@[simp]

theorem nat.find_eq_zero {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :

nat.find h = 0 ↔ p 0

theorem nat.find_mono {p q : ℕ → Prop} [decidable_pred p] [decidable_pred q] (h : ∀ (n : ℕ), q n → p n) {hp : ∃ (n : ℕ), p n} {hq : ∃ (n : ℕ), q n} :

nat.find hp ≤ nat.find hq

theorem nat.find_le {n : ℕ} {p : ℕ → Prop} [decidable_pred p] {h : ∃ (n : ℕ), p n} (hn : p n) :

nat.find h ≤ n

theorem nat.find_comp_succ {p : ℕ → Prop} [decidable_pred p] (h₁ : ∃ (n : ℕ), p n) (h₂ : ∃ (n : ℕ), p (n + 1)) (h0 : ¬p 0) :

nat.find h₁ = nat.find h₂ + 1

`find_greatest` #

@[protected]

def nat.find_greatest (P : ℕ → Prop) [decidable_pred P] :

find_greatest P b is the largest i ≤ bound such that P i holds, or 0 if no such i exists

Equations

nat.find_greatest P (n + 1) = ite (P (n + 1)) (n + 1) (nat.find_greatest P n)
nat.find_greatest P 0 = 0

@[simp]

theorem nat.find_greatest_zero {P : ℕ → Prop} [decidable_pred P] :

nat.find_greatest P 0 = 0

theorem nat.find_greatest_succ {P : ℕ → Prop} [decidable_pred P] (n : ℕ) :

nat.find_greatest P (n + 1) = ite (P (n + 1)) (n + 1) (nat.find_greatest P n)

@[simp]

theorem nat.find_greatest_eq {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :

P b → nat.find_greatest P b = b

@[simp]

theorem nat.find_greatest_of_not {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (h : ¬P (b + 1)) :

nat.find_greatest P (b + 1) = nat.find_greatest P b

decidability of predicates #

@[protected, instance]

def nat.decidable_ball_lt (n : ℕ) (P : Π (k : ℕ), k < n → Prop) [H : Π (n_1 : ℕ) (h : n_1 < n), decidable (P n_1 h)] :

decidable (∀ (n_1 : ℕ) (h : n_1 < n), P n_1 h)

Equations

n.decidable_ball_lt P = nat.rec (λ (P : Π (k : ℕ), k < 0 → Prop) (H : Π (n : ℕ) (h : n < 0), decidable (P n h)), decidable.is_true _) (λ (n : ℕ) (IH : Π (P : Π (k : ℕ), k < n → Prop) [H : Π (n_1 : ℕ) (h : n_1 < n), decidable (P n_1 h)], decidable (∀ (n_1 : ℕ) (h : n_1 < n), P n_1 h)) (P : Π (k : ℕ), k < n.succ → Prop) (H : Π (n_1 : ℕ) (h : n_1 < n.succ), decidable (P n_1 h)), (IH (λ (k : ℕ) (h : k < n), P k _)).cases_on (λ (h : ¬∀ (n_1 : ℕ) (h : n_1 < n), (λ (k : ℕ) (h : k < n), P k _) n_1 h), decidable.is_false _) (λ (h : ∀ (n_1 : ℕ) (h : n_1 < n), (λ (k : ℕ) (h : k < n), P k _) n_1 h), dite (P n _) (λ (p : P n _), decidable.is_true _) (λ (p : ¬P n _), decidable.is_false _))) n P

@[protected, instance]

def nat.decidable_forall_fin {n : ℕ} (P : fin n → Prop) [H : decidable_pred P] :

decidable (∀ (i : fin n), P i)

Equations

nat.decidable_forall_fin P = decidable_of_iff (∀ (k : ℕ) (h : k < n), P ⟨k, h⟩) _

@[protected, instance]

def nat.decidable_ball_le (n : ℕ) (P : Π (k : ℕ), k ≤ n → Prop) [H : Π (n_1 : ℕ) (h : n_1 ≤ n), decidable (P n_1 h)] :

decidable (∀ (n_1 : ℕ) (h : n_1 ≤ n), P n_1 h)

Equations

n.decidable_ball_le P = decidable_of_iff (∀ (k : ℕ) (h : k < n.succ), P k _) _

@[protected, instance]

def nat.decidable_exists_lt {P : ℕ → Prop} [h : decidable_pred P] :

decidable_pred (λ (n : ℕ), ∃ (m : ℕ), m < n ∧ P m)

Equations

nat.decidable_exists_lt (n + 1) = decidable_of_decidable_of_iff or.decidable _
nat.decidable_exists_lt 0 = decidable.is_false nat.decidable_exists_lt._main._proof_1

@[protected, instance]

def nat.decidable_exists_le {P : ℕ → Prop} [h : decidable_pred P] :

decidable_pred (λ (n : ℕ), ∃ (m : ℕ), m ≤ n ∧ P m)

Equations

nat.decidable_exists_le = λ (n : ℕ), decidable_of_iff (∃ (m : ℕ), m < n + 1 ∧ P m) _