Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro

! This file was ported from Lean 3 source module data.nat.basic
! leanprover-community/mathlib commit bd835ef554f37ef9b804f0903089211f89cb370b
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Basic
import Mathlib.Algebra.GroupWithZero.Basic
import Mathlib.Algebra.Ring.Defs

/-!
# Basic operations on the natural numbers

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.


-/


universe u v

namespace Nat

/-! ### instances -/

instance 
nontrivial: Nontrivial β„•
nontrivial
:
Nontrivial: Type ?u.2 β†’ Prop
Nontrivial
β„•: Type
β„•
:= ⟨⟨
0: ?m.22
0
,
1: ?m.42
1
,
Nat.zero_ne_one: 0 β‰  1
Nat.zero_ne_one
⟩⟩ instance
commSemiring: CommSemiring β„•
commSemiring
:
CommSemiring: Type ?u.55 β†’ Type ?u.55
CommSemiring
β„•: Type
β„•
where add :=
Nat.add: β„• β†’ β„• β†’ β„•
Nat.add
add_assoc :=
Nat.add_assoc: βˆ€ (n m k : β„•), n + m + k = n + (m + k)
Nat.add_assoc
zero :=
Nat.zero: β„•
Nat.zero
zero_add :=
Nat.zero_add: βˆ€ (n : β„•), 0 + n = n
Nat.zero_add
add_zero :=
Nat.add_zero: βˆ€ (n : β„•), n + 0 = n
Nat.add_zero
add_comm :=
Nat.add_comm: βˆ€ (n m : β„•), n + m = m + n
Nat.add_comm
mul :=
Nat.mul: β„• β†’ β„• β†’ β„•
Nat.mul
mul_assoc :=
Nat.mul_assoc: βˆ€ (n m k : β„•), n * m * k = n * (m * k)
Nat.mul_assoc
one :=
Nat.succ: β„• β†’ β„•
Nat.succ
Nat.zero: β„•
Nat.zero
one_mul :=
Nat.one_mul: βˆ€ (n : β„•), 1 * n = n
Nat.one_mul
mul_one :=
Nat.mul_one: βˆ€ (n : β„•), n * 1 = n
Nat.mul_one
left_distrib :=
Nat.left_distrib: βˆ€ (n m k : β„•), n * (m + k) = n * m + n * k
Nat.left_distrib
right_distrib :=
Nat.right_distrib: βˆ€ (n m k : β„•), (n + m) * k = n * k + m * k
Nat.right_distrib
zero_mul :=
Nat.zero_mul: βˆ€ (n : β„•), 0 * n = 0
Nat.zero_mul
mul_zero :=
Nat.mul_zero: βˆ€ (n : β„•), n * 0 = 0
Nat.mul_zero
mul_comm :=
Nat.mul_comm: βˆ€ (n m : β„•), n * m = m * n
Nat.mul_comm
natCast
n: ?m.275
n
:=
n: ?m.275
n
natCast_zero :=
rfl: βˆ€ {Ξ± : Sort ?u.279} {a : Ξ±}, a = a
rfl
natCast_succ
n: ?m.283
n
:=
rfl: βˆ€ {Ξ± : Sort ?u.285} {a : Ξ±}, a = a
rfl
nsmul
m: ?m.111
m
n: ?m.114
n
:=
m: ?m.111
m
*
n: ?m.114
n
nsmul_zero :=
Nat.zero_mul: βˆ€ (n : β„•), 0 * n = 0
Nat.zero_mul
nsmul_succ
_: ?m.172
_
_: ?m.175
_
:=

Goals accomplished! πŸ™
x✝¹, x✝: β„•


(fun m n => m * n) (x✝¹ + 1) x✝ = x✝ + (fun m n => m * n) x✝¹ x✝
x✝¹, x✝: β„•


(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
x✝¹, x✝: β„•


(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
x✝¹, x✝: β„•


(fun m n => m * n) (x✝¹ + 1) x✝ = x✝ + (fun m n => m * n) x✝¹ x✝
x✝¹, x✝: β„•


(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
x✝¹, x✝: β„•


(1 + x✝¹) * x✝ = x✝ + x✝¹ * x✝
x✝¹, x✝: β„•


(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
x✝¹, x✝: β„•


1 * x✝ + x✝¹ * x✝ = x✝ + x✝¹ * x✝
x✝¹, x✝: β„•


(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
x✝¹, x✝: β„•


x✝ + x✝¹ * x✝ = x✝ + x✝¹ * x✝

Goals accomplished! πŸ™
npow
m: ?m.293
m
n: ?m.296
n
:=
n: ?m.296
n
^
m: ?m.293
m
npow_zero :=
Nat.pow_zero: βˆ€ (n : β„•), n ^ 0 = 1
Nat.pow_zero
npow_succ
_: ?m.350
_
_: ?m.353
_
:=
Nat.pow_succ': βˆ€ {m n : β„•}, m ^ succ n = m * m ^ n
Nat.pow_succ'
/-! Extra instances to short-circuit type class resolution and ensure computability -/ instance
addCommMonoid: AddCommMonoid β„•
addCommMonoid
:
AddCommMonoid: Type ?u.892 β†’ Type ?u.892
AddCommMonoid
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.894} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
addMonoid: AddMonoid β„•
addMonoid
:
AddMonoid: Type ?u.1154 β†’ Type ?u.1154
AddMonoid
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.1156} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
monoid: Monoid β„•
monoid
:
Monoid: Type ?u.1406 β†’ Type ?u.1406
Monoid
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.1408} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
commMonoid: CommMonoid β„•
commMonoid
:
CommMonoid: Type ?u.1586 β†’ Type ?u.1586
CommMonoid
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.1588} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
commSemigroup: CommSemigroup β„•
commSemigroup
:
CommSemigroup: Type ?u.1721 β†’ Type ?u.1721
CommSemigroup
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.1723} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
semigroup: Semigroup β„•
semigroup
:
Semigroup: Type ?u.1890 β†’ Type ?u.1890
Semigroup
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.1892} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
addCommSemigroup: AddCommSemigroup β„•
addCommSemigroup
:
AddCommSemigroup: Type ?u.2056 β†’ Type ?u.2056
AddCommSemigroup
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.2058} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
addSemigroup: AddSemigroup β„•
addSemigroup
:
AddSemigroup: Type ?u.2156 β†’ Type ?u.2156
AddSemigroup
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.2158} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
distrib: Distrib β„•
distrib
:
Distrib: Type ?u.2244 β†’ Type ?u.2244
Distrib
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.2246} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
instance
semiring: Semiring β„•
semiring
:
Semiring: Type ?u.2414 β†’ Type ?u.2414
Semiring
β„•: Type
β„•
:=
inferInstance: {Ξ± : Sort ?u.2416} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
protected theorem
nsmul_eq_mul: βˆ€ (m n : β„•), m β€’ n = m * n
nsmul_eq_mul
(m n :
β„•: Type
β„•
) : m β€’ n = m * n :=
rfl: βˆ€ {Ξ± : Sort ?u.2602} {a : Ξ±}, a = a
rfl
#align nat.nsmul_eq_mul
Nat.nsmul_eq_mul: βˆ€ (m n : β„•), m β€’ n = m * n
Nat.nsmul_eq_mul
-- Moved to core #align nat.eq_of_mul_eq_mul_right
Nat.eq_of_mul_eq_mul_right: βˆ€ {n m k : β„•}, 0 < m β†’ n * m = k * m β†’ n = k
Nat.eq_of_mul_eq_mul_right
instance
cancelCommMonoidWithZero: CancelCommMonoidWithZero β„•
cancelCommMonoidWithZero
:
CancelCommMonoidWithZero: Type ?u.2611 β†’ Type ?u.2611
CancelCommMonoidWithZero
β„•: Type
β„•
:= { (
inferInstance: {Ξ± : Sort ?u.2617} β†’ [i : Ξ±] β†’ Ξ±
inferInstance
:
CommMonoidWithZero: Type ?u.2616 β†’ Type ?u.2616
CommMonoidWithZero
β„•: Type
β„•
) with mul_left_cancel_of_ne_zero := fun
h1: ?m.2697
h1
h2: ?m.2700
h2
=>
Nat.eq_of_mul_eq_mul_left: βˆ€ {m k n : β„•}, 0 < n β†’ n * m = n * k β†’ m = k
Nat.eq_of_mul_eq_mul_left
(
Nat.pos_of_ne_zero: βˆ€ {n : β„•}, n β‰  0 β†’ 0 < n
Nat.pos_of_ne_zero
h1: ?m.2697
h1
)
h2: ?m.2700
h2
} #align nat.cancel_comm_monoid_with_zero
Nat.cancelCommMonoidWithZero: CancelCommMonoidWithZero β„•
Nat.cancelCommMonoidWithZero
attribute [simp]
Nat.not_lt_zero: βˆ€ (n : β„•), Β¬n < 0
Nat.not_lt_zero
Nat.succ_ne_zero: βˆ€ (n : β„•), succ n β‰  0
Nat.succ_ne_zero
Nat.succ_ne_self: βˆ€ (n : β„•), succ n β‰  n
Nat.succ_ne_self
Nat.zero_ne_one: 0 β‰  1
Nat.zero_ne_one
Nat.one_ne_zero: 1 β‰  0
Nat.one_ne_zero
-- Nat.zero_ne_bit1 Nat.bit1_ne_zero Nat.bit0_ne_one Nat.one_ne_bit0 Nat.bit0_ne_bit1 -- Nat.bit1_ne_bit0 variable {m n k :
β„•: Type
β„•
} /-! ### Recursion and `forall`/`exists` -/ -- Porting note: -- this doesn't work as a simp lemma in Lean 4 -- @[simp] theorem
and_forall_succ: βˆ€ {p : β„• β†’ Prop}, (p 0 ∧ βˆ€ (n : β„•), p (n + 1)) ↔ βˆ€ (n : β„•), p n
and_forall_succ
{
p: β„• β†’ Prop
p
:
β„•: Type
β„•
β†’
Prop: Type
Prop
} : (
p: β„• β†’ Prop
p
0: ?m.2960
0
∧ βˆ€
n: ?m.2971
n
,
p: β„• β†’ Prop
p
(
n: ?m.2971
n
+
1: ?m.2978
1
)) ↔ βˆ€
n: ?m.3033
n
,
p: β„• β†’ Prop
p
n: ?m.3033
n
:= ⟨fun
h: ?m.3055
h
n: ?m.3058
n
=>
Nat.casesOn: βˆ€ {motive : β„• β†’ Sort ?u.3060} (t : β„•), motive zero β†’ (βˆ€ (n : β„•), motive (succ n)) β†’ motive t
Nat.casesOn
n: ?m.3058
n
h: ?m.3055
h
.
1: βˆ€ {a b : Prop}, a ∧ b β†’ a
1
h: ?m.3055
h
.
2: βˆ€ {a b : Prop}, a ∧ b β†’ b
2
, fun
h: ?m.3086
h
=> ⟨
h: ?m.3086
h
_, fun
_: ?m.3100
_
=>
h: ?m.3086
h
_⟩⟩ #align nat.and_forall_succ
Nat.and_forall_succ: βˆ€ {p : β„• β†’ Prop}, (p 0 ∧ βˆ€ (n : β„•), p (n + 1)) ↔ βˆ€ (n : β„•), p n
Nat.and_forall_succ
-- Porting note: -- this doesn't work as a simp lemma in Lean 4 -- @[simp] theorem
or_exists_succ: βˆ€ {p : β„• β†’ Prop}, (p 0 ∨ βˆƒ n, p (n + 1)) ↔ βˆƒ n, p n
or_exists_succ
{
p: β„• β†’ Prop
p
:
β„•: Type
β„•
β†’
Prop: Type
Prop
} : (
p: β„• β†’ Prop
p
0: ?m.3136
0
∨ βˆƒ
n: ?m.3149
n
,
p: β„• β†’ Prop
p
(
n: ?m.3149
n
+
1: ?m.3155
1
)) ↔ βˆƒ
n: ?m.3213
n
,
p: β„• β†’ Prop
p
n: ?m.3213
n
:= ⟨fun
h: ?m.3234
h
=>
h: ?m.3234
h
.
elim: βˆ€ {a b c : Prop}, a ∨ b β†’ (a β†’ c) β†’ (b β†’ c) β†’ c
elim
(fun
h0: ?m.3248
h0
=> ⟨
0: ?m.3263
0
,
h0: ?m.3248
h0
⟩) fun ⟨n,
hn: p (n + 1)
hn
⟩ => ⟨n +
1: ?m.3310
1
,
hn: p (n + 1)
hn
⟩,

Goals accomplished! πŸ™
m, n, k: β„•

p: β„• β†’ Prop


(βˆƒ n, p n) β†’ p 0 ∨ βˆƒ n, p (n + 1)
m, n, k: β„•

p: β„• β†’ Prop

hn: p zero


intro.zero
p 0 ∨ βˆƒ n, p (n + 1)
m, n✝, k: β„•

p: β„• β†’ Prop

n: β„•

hn: p (succ n)


intro.succ
p 0 ∨ βˆƒ n, p (n + 1)
m, n, k: β„•

p: β„• β†’ Prop


(βˆƒ n, p n) β†’ p 0 ∨ βˆƒ n, p (n + 1)

Goals accomplished! πŸ™
⟩ #align nat.or_exists_succ
Nat.or_exists_succ: βˆ€ {p : β„• β†’ Prop}, (p 0 ∨ βˆƒ n, p (n + 1)) ↔ βˆƒ n, p n
Nat.or_exists_succ
/-! ### `succ` -/ theorem
_root_.LT.lt.nat_succ_le: βˆ€ {n m : β„•}, n < m β†’ succ n ≀ m
_root_.LT.lt.nat_succ_le
{n m :
β„•: Type
β„•
} (
h: n < m
h
: n < m) :
succ: β„• β†’ β„•
succ
n ≀ m :=
succ_le_of_lt: βˆ€ {n m : β„•}, n < m β†’ succ n ≀ m
succ_le_of_lt
h: n < m
h
#align has_lt.lt.nat_succ_le
LT.lt.nat_succ_le: βˆ€ {n m : β„•}, n < m β†’ succ n ≀ m
LT.lt.nat_succ_le
-- Moved to Std #align nat.succ_eq_one_add
Nat.succ_eq_one_add: βˆ€ (n : β„•), succ n = 1 + n
Nat.succ_eq_one_add
theorem
eq_of_lt_succ_of_not_lt: βˆ€ {a b : β„•}, a < b + 1 β†’ Β¬a < b β†’ a = b
eq_of_lt_succ_of_not_lt
{a b :
β„•: Type
β„•
} (
h1: a < b + 1
h1
: a < b +
1: ?m.3569
1
) (
h2: Β¬a < b
h2
: Β¬a < b) : a = b := have
h3: a ≀ b
h3
: a ≀ b :=
le_of_lt_succ: βˆ€ {m n : β„•}, m < succ n β†’ m ≀ n
le_of_lt_succ
h1: a < b + 1
h1
Or.elim: βˆ€ {a b c : Prop}, a ∨ b β†’ (a β†’ c) β†’ (b β†’ c) β†’ c
Or.elim
(
eq_or_lt_of_not_lt: βˆ€ {Ξ± : Type ?u.3667} [inst : LinearOrder Ξ±] {a b : Ξ±}, Β¬a < b β†’ a = b ∨ b < a
eq_or_lt_of_not_lt
h2: Β¬a < b
h2
) (fun
h: ?m.3690
h
=>
h: ?m.3690
h
) fun
h: ?m.3695
h
=>
absurd: βˆ€ {a : Prop} {b : Sort ?u.3697}, a β†’ Β¬a β†’ b
absurd
h: ?m.3695
h
(
not_lt_of_ge: βˆ€ {Ξ± : Type ?u.3700} [inst : Preorder Ξ±] {a b : Ξ±}, a β‰₯ b β†’ Β¬a < b
not_lt_of_ge
h3: a ≀ b
h3
) #align nat.eq_of_lt_succ_of_not_lt
Nat.eq_of_lt_succ_of_not_lt: βˆ€ {a b : β„•}, a < b + 1 β†’ Β¬a < b β†’ a = b
Nat.eq_of_lt_succ_of_not_lt
theorem
eq_of_le_of_lt_succ: βˆ€ {n m : β„•}, n ≀ m β†’ m < n + 1 β†’ m = n
eq_of_le_of_lt_succ
{n m :
β„•: Type
β„•
} (
h₁: n ≀ m
h₁
: n ≀ m) (
hβ‚‚: m < n + 1
hβ‚‚
: m < n +
1: ?m.3770
1
) : m = n :=
Nat.le_antisymm: βˆ€ {n m : β„•}, n ≀ m β†’ m ≀ n β†’ n = m
Nat.le_antisymm
(
le_of_succ_le_succ: βˆ€ {n m : β„•}, succ n ≀ succ m β†’ n ≀ m
le_of_succ_le_succ
hβ‚‚: m < n + 1
hβ‚‚
)
h₁: n ≀ m
h₁
#align nat.eq_of_le_of_lt_succ
Nat.eq_of_le_of_lt_succ: βˆ€ {n m : β„•}, n ≀ m β†’ m < n + 1 β†’ m = n
Nat.eq_of_le_of_lt_succ
-- Moved to Std #align nat.one_add
Nat.one_add: βˆ€ (n : β„•), 1 + n = succ n
Nat.one_add
@[simp] theorem
succ_pos': βˆ€ {n : β„•}, 0 < succ n
succ_pos'
{n :
β„•: Type
β„•
} :
0: ?m.3872
0
<
succ: β„• β†’ β„•
succ
n :=
succ_pos: βˆ€ (n : β„•), 0 < succ n
succ_pos
n #align nat.succ_pos'
Nat.succ_pos': βˆ€ {n : β„•}, 0 < succ n
Nat.succ_pos'
-- Moved to Std #align nat.succ_inj'
Nat.succ_inj': βˆ€ {n m : β„•}, succ n = succ m ↔ n = m
Nat.succ_inj'
theorem
succ_injective: Function.Injective succ
succ_injective
:
Function.Injective: {Ξ± : Sort ?u.3928} β†’ {Ξ² : Sort ?u.3927} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective
Nat.succ: β„• β†’ β„•
Nat.succ
:= fun
_: ?m.3936
_
_: ?m.3939
_
=>
succ.inj: βˆ€ {n n_1 : β„•}, succ n = succ n_1 β†’ n = n_1
succ.inj
#align nat.succ_injective
Nat.succ_injective: Function.Injective succ
Nat.succ_injective
theorem
succ_ne_succ: βˆ€ {n m : β„•}, succ n β‰  succ m ↔ n β‰  m
succ_ne_succ
{n m :
β„•: Type
β„•
} :
succ: β„• β†’ β„•
succ
n β‰ 
succ: β„• β†’ β„•
succ
m ↔ n β‰  m :=
succ_injective: Function.Injective succ
succ_injective
.
ne_iff: βˆ€ {Ξ± : Sort ?u.3971} {Ξ² : Sort ?u.3972} {f : Ξ± β†’ Ξ²}, Function.Injective f β†’ βˆ€ {x y : Ξ±}, f x β‰  f y ↔ x β‰  y
ne_iff
#align nat.succ_ne_succ
Nat.succ_ne_succ: βˆ€ {n m : β„•}, succ n β‰  succ m ↔ n β‰  m
Nat.succ_ne_succ
-- Porting note: no longer a simp lemma, as simp can prove this theorem
succ_succ_ne_one: βˆ€ (n : β„•), succ (succ n) β‰  1
succ_succ_ne_one
(n :
β„•: Type
β„•
) : n.
succ: β„• β†’ β„•
succ
.
succ: β„• β†’ β„•
succ
β‰ 
1: ?m.4009
1
:=
succ_ne_succ: βˆ€ {n m : β„•}, succ n β‰  succ m ↔ n β‰  m
succ_ne_succ
.
mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
mpr
n.
succ_ne_zero: βˆ€ (n : β„•), succ n β‰  0
succ_ne_zero
#align nat.succ_succ_ne_one
Nat.succ_succ_ne_one: βˆ€ (n : β„•), succ (succ n) β‰  1
Nat.succ_succ_ne_one
@[simp] theorem
one_lt_succ_succ: βˆ€ (n : β„•), 1 < succ (succ n)
one_lt_succ_succ
(n :
β„•: Type
β„•
) :
1: ?m.4064
1
< n.
succ: β„• β†’ β„•
succ
.
succ: β„• β†’ β„•
succ
:=
succ_lt_succ: βˆ€ {n m : β„•}, n < m β†’ succ n < succ m
succ_lt_succ
<|
succ_pos: βˆ€ (n : β„•), 0 < succ n
succ_pos
n #align nat.one_lt_succ_succ
Nat.one_lt_succ_succ: βˆ€ (n : β„•), 1 < succ (succ n)
Nat.one_lt_succ_succ
-- Porting note: Nat.succ_le_succ_iff is in Std theorem
max_succ_succ: βˆ€ {m n : β„•}, max (succ m) (succ n) = succ (max m n)
max_succ_succ
{m n :
β„•: Type
β„•
} :
max: {Ξ± : Type ?u.4149} β†’ [self : Max Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ξ±
max
(
succ: β„• β†’ β„•
succ
m) (
succ: β„• β†’ β„•
succ
n) =
succ: β„• β†’ β„•
succ
(
max: {Ξ± : Type ?u.4155} β†’ [self : Max Ξ±] β†’ Ξ± β†’ Ξ± β†’ Ξ±
max
m n) :=

Goals accomplished! πŸ™
m✝, n✝, k, m, n: β„•


max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: m ≀ n


pos
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•


max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: m ≀ n


pos
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: m ≀ n


pos
max (succ m) (succ n) = succ n
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: m ≀ n


pos
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: m ≀ n


pos
succ n = succ n
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•


max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: n < m


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: n < m


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: n < m


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: n < m

h2: n ≀ m


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: Β¬m ≀ n


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: n < m

h2: n ≀ m


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: n < m

h2: n ≀ m


neg
max (succ m) (succ n) = succ m
m✝, n✝, k, m, n: β„•

h1: n < m

h2: n ≀ m


neg
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: β„•

h1: n < m

h2: n ≀ m


neg
succ m = succ m

Goals accomplished! πŸ™
#align nat.max_succ_succ
Nat.max_succ_succ: βˆ€ {m n : β„•}, max (succ m) (succ n) = succ (max m n)
Nat.max_succ_succ
theorem
not_succ_lt_self: βˆ€ {n : β„•}, Β¬succ n < n
not_succ_lt_self
{n :
β„•: Type
β„•
} : Β¬
succ: β„• β†’ β„•
succ
n < n :=
not_lt_of_ge: βˆ€ {Ξ± : Type ?u.4396} [inst : Preorder Ξ±] {a b : Ξ±}, a β‰₯ b β†’ Β¬a < b
not_lt_of_ge
(
Nat.le_succ: βˆ€ (n : β„•), n ≀ succ n
Nat.le_succ
_) #align nat.not_succ_lt_self
Nat.not_succ_lt_self: βˆ€ {n : β„•}, Β¬succ n < n
Nat.not_succ_lt_self
theorem
lt_succ_iff: βˆ€ {m n : β„•}, m < succ n ↔ m ≀ n
lt_succ_iff
{m n :
β„•: Type
β„•
} : m <
succ: β„• β†’ β„•
succ
n ↔ m ≀ n := ⟨
le_of_lt_succ: βˆ€ {m n : β„•}, m < succ n β†’ m ≀ n
le_of_lt_succ
,
lt_succ_of_le: βˆ€ {n m : β„•}, n ≀ m β†’ n < succ m
lt_succ_of_le
⟩ #align nat.lt_succ_iff
Nat.lt_succ_iff: βˆ€ {m n : β„•}, m < succ n ↔ m ≀ n
Nat.lt_succ_iff
theorem
succ_le_iff: βˆ€ {m n : β„•}, succ m ≀ n ↔ m < n
succ_le_iff
{m n :
β„•: Type
β„•
} :
succ: β„• β†’ β„•
succ
m ≀ n ↔ m < n := ⟨
lt_of_succ_le: βˆ€ {n m : β„•}, succ n ≀ m β†’ n < m
lt_of_succ_le
,
succ_le_of_lt: βˆ€ {n m : β„•}, n < m β†’ succ n ≀ m
succ_le_of_lt
⟩ #align nat.succ_le_iff
Nat.succ_le_iff: βˆ€ {m n : β„•}, succ m ≀ n ↔ m < n
Nat.succ_le_iff
theorem
lt_iff_add_one_le: βˆ€ {m n : β„•}, m < n ↔ m + 1 ≀ n
lt_iff_add_one_le
{m n :
β„•: Type
β„•
} : m < n ↔ m +
1: ?m.4569
1
≀ n :=

Goals accomplished! πŸ™
m✝, n✝, k, m, n: β„•


m < n ↔ m + 1 ≀ n
m✝, n✝, k, m, n: β„•


m < n ↔ m + 1 ≀ n
m✝, n✝, k, m, n: β„•


m < n ↔ m < n

Goals accomplished! πŸ™
#align nat.lt_iff_add_one_le
Nat.lt_iff_add_one_le: βˆ€ {m n : β„•}, m < n ↔ m + 1 ≀ n
Nat.lt_iff_add_one_le
-- Just a restatement of `Nat.lt_succ_iff` using `+1`. theorem
lt_add_one_iff: βˆ€ {a b : β„•}, a < b + 1 ↔ a ≀ b
lt_add_one_iff
{a b :
β„•: Type
β„•
} : a < b +
1: ?m.4678
1
↔ a ≀ b :=
lt_succ_iff: βˆ€ {m n : β„•}, m < succ n ↔ m ≀ n
lt_succ_iff
#align nat.lt_add_one_iff
Nat.lt_add_one_iff: βˆ€ {a b : β„•}, a < b + 1 ↔ a ≀ b
Nat.lt_add_one_iff
-- A flipped version of `lt_add_one_iff`. theorem
lt_one_add_iff: βˆ€ {a b : β„•}, a < 1 + b ↔ a ≀ b
lt_one_add_iff
{a b :
β„•: Type
β„•
} : a <
1: ?m.4780
1
+ b ↔ a ≀ b :=

Goals accomplished! πŸ™
m, n, k, a, b: β„•


a < 1 + b ↔ a ≀ b

Goals accomplished! πŸ™
#align nat.lt_one_add_iff
Nat.lt_one_add_iff: βˆ€ {a b : β„•}, a < 1 + b ↔ a ≀ b
Nat.lt_one_add_iff
-- This is true reflexively, by the definition of `≀` on β„•, -- but it's still useful to have, to convince Lean to change the syntactic type. theorem
add_one_le_iff: βˆ€ {a b : β„•}, a + 1 ≀ b ↔ a < b
add_one_le_iff
{a b :
β„•: Type
β„•
} : a +
1: ?m.5016
1
≀ b ↔ a < b :=
Iff.refl: βˆ€ (a : Prop), a ↔ a
Iff.refl
_: Prop
_
#align nat.add_one_le_iff
Nat.add_one_le_iff: βˆ€ {a b : β„•}, a + 1 ≀ b ↔ a < b
Nat.add_one_le_iff
theorem
one_add_le_iff: βˆ€ {a b : β„•}, 1 + a ≀ b ↔ a < b
one_add_le_iff
{a b :
β„•: Type
β„•
} :
1: ?m.5118
1
+ a ≀ b ↔ a < b :=

Goals accomplished! πŸ™
m, n, k, a, b: β„•


1 + a ≀ b ↔ a < b

Goals accomplished! πŸ™
#align nat.one_add_le_iff
Nat.one_add_le_iff: βˆ€ {a b : β„•}, 1 + a ≀ b ↔ a < b
Nat.one_add_le_iff
theorem
of_le_succ: βˆ€ {n m : β„•}, n ≀ succ m β†’ n ≀ m ∨ n = succ m
of_le_succ
{n m :
β„•: Type
β„•
} (
H: n ≀ succ m
H
: n ≀ m.
succ: β„• β†’ β„•
succ
) : n ≀ m ∨ n = m.
succ: β„• β†’ β„•
succ
:=
H: n ≀ succ m
H
.
lt_or_eq_dec: βˆ€ {Ξ± : Type ?u.5377} [inst : PartialOrder Ξ±] [inst_1 : DecidableRel fun x x_1 => x ≀ x_1] {a b : Ξ±}, a ≀ b β†’ a < b ∨ a = b
lt_or_eq_dec
.
imp: βˆ€ {a c b d : Prop}, (a β†’ c) β†’ (b β†’ d) β†’ a ∨ b β†’ c ∨ d
imp
le_of_lt_succ: βˆ€ {m n : β„•}, m < succ n β†’ m ≀ n
le_of_lt_succ
id: βˆ€ {Ξ± : Sort ?u.5449}, Ξ± β†’ Ξ±
id
#align nat.of_le_succ
Nat.of_le_succ: βˆ€ {n m : β„•}, n ≀ succ m β†’ n ≀ m ∨ n = succ m
Nat.of_le_succ
theorem
succ_lt_succ_iff: βˆ€ {m n : β„•}, succ m < succ n ↔ m < n
succ_lt_succ_iff
{m n :
β„•: Type
β„•
} :
succ: β„• β†’ β„•
succ
m <
succ: β„• β†’ β„•
succ
n ↔ m < n := ⟨
lt_of_succ_lt_succ: βˆ€ {n m : β„•}, succ n < succ m β†’ n < m
lt_of_succ_lt_succ
,
succ_lt_succ: βˆ€ {n m : β„•}, n < m β†’ succ n < succ m
succ_lt_succ
⟩ #align nat.succ_lt_succ_iff
Nat.succ_lt_succ_iff: βˆ€ {m n : β„•}, succ m < succ n ↔ m < n
Nat.succ_lt_succ_iff
theorem
div_le_iff_le_mul_add_pred: βˆ€ {m n k : β„•}, 0 < n β†’ (m / n ≀ k ↔ m ≀ n * k + (n - 1))
div_le_iff_le_mul_add_pred
{m n k :
β„•: Type
β„•
} (
n0: 0 < n
n0
:
0: ?m.5521
0
< n) : m / n ≀ k ↔ m ≀ n * k + (n -
1: ?m.5613
1
) :=

Goals accomplished! πŸ™
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m / n ≀ k ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m / n ≀ k ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m / n < succ k ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m / n ≀ k ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m < succ k * n ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m / n ≀ k ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m < k * n + n ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m / n ≀ k ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m < n * k + n ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m < n * k + n ↔ m ≀ n * k + (n - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m / n ≀ k ↔ m ≀ n * k + (n - 1)
m✝, n, k✝, m, k: β„•

n0: 0 < zero


zero
m✝, n, k✝, m, k, n✝: β„•

n0: 0 < succ n✝


succ
m < succ n✝ * k + succ n✝ ↔ m ≀ succ n✝ * k + (succ n✝ - 1)
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


m / n ≀ k ↔ m ≀ n * k + (n - 1)
m✝, n, k✝, m, k: β„•

n0: 0 < zero


zero
m✝, n, k✝, m, k: β„•

n0: 0 < zero


zero
m✝, n, k✝, m, k, n✝: β„•

n0: 0 < succ n✝


succ
m < succ n✝ * k + succ n✝ ↔ m ≀ succ n✝ * k + (succ n✝ - 1)

Goals accomplished! πŸ™
m✝, n✝, k✝, m, n, k: β„•

n0: 0 < n


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

Goals accomplished! πŸ™
#align nat.div_le_iff_le_mul_add_pred
Nat.div_le_iff_le_mul_add_pred: βˆ€ {m n k : β„•}, 0 < n β†’ (m / n ≀ k ↔ m ≀ n * k + (n - 1))
Nat.div_le_iff_le_mul_add_pred
theorem
two_lt_of_ne: βˆ€ {n : β„•}, n β‰  0 β†’ n β‰  1 β†’ n β‰  2 β†’ 2 < n
two_lt_of_ne
: βˆ€ {
n: ?m.6021
n
},
n: ?m.6021
n
β‰ 
0: ?m.6028
0
β†’
n: ?m.6021
n
β‰ 
1: ?m.6044
1
β†’
n: ?m.6021
n
β‰ 
2: ?m.6057
2
β†’
2: ?m.6067
2
<
n: ?m.6021
n
| 0,
h: 0 β‰  0
h
, _, _ => (
h: 0 β‰  0
h
rfl: βˆ€ {Ξ± : Sort ?u.6259} {a : Ξ±}, a = a
rfl
).
elim: βˆ€ {C : Sort ?u.6265}, False β†’ C
elim
| 1, _,
h: 1 β‰  1
h
, _ => (
h: 1 β‰  1
h
rfl: βˆ€ {Ξ± : Sort ?u.6299} {a : Ξ±}, a = a
rfl
).
elim: βˆ€ {C : Sort ?u.6302}, False β†’ C
elim
| 2, _, _,
h: 2 β‰  2
h
=> (
h: 2 β‰  2
h
rfl: βˆ€ {Ξ± : Sort ?u.6336} {a : Ξ±}, a = a
rfl
).
elim: βˆ€ {C : Sort ?u.6339}, False β†’ C
elim
-- Porting note: was `by decide` | n + 3, _, _, _ =>

Goals accomplished! πŸ™
m, n✝, k, n: β„•

x✝²: n + 3 β‰  0

x✝¹: n + 3 β‰  1

x✝: n + 3 β‰  2


2 < n + 3
m, n✝, k, n: β„•

x✝²: n + 3 β‰  0

x✝¹: n + 3 β‰  1

x✝: n + 3 β‰  2


2 < n + 3
m, n✝, k, n: β„•

x✝²: n + 3 β‰  0

x✝¹: n + 3 β‰  1

x✝: n + 3 β‰  2


2 + 1 ≀ n + 3
m, n✝, k, n: β„•

x✝²: n + 3 β‰  0

x✝¹: n + 3 β‰  1

x✝: n + 3 β‰  2


2 + 1 ≀ n + 3
m, n✝, k, n: β„•

x✝²: n + 3 β‰  0

x✝¹: n + 3 β‰  1

x✝: n + 3 β‰  2


2 + 1 ≀ n + 3
m, n✝, k, n: β„•

x✝²: n + 3 β‰  0

x✝¹: n + 3 β‰  1

x✝: n + 3 β‰  2


2 < n + 3

Goals accomplished! πŸ™
#align nat.two_lt_of_ne
Nat.two_lt_of_ne: βˆ€ {n : β„•}, n β‰  0 β†’ n β‰  1 β†’ n β‰  2 β†’ 2 < n
Nat.two_lt_of_ne
theorem
forall_lt_succ: βˆ€ {P : β„• β†’ Prop} {n : β„•}, (βˆ€ (m : β„•), m < n + 1 β†’ P m) ↔ (βˆ€ (m : β„•), m < n β†’ P m) ∧ P n
forall_lt_succ
{
P: β„• β†’ Prop
P
:
β„•: Type
β„•
β†’
Prop: Type
Prop
} {n :
β„•: Type
β„•
} : (βˆ€
m: ?m.6925
m
< n +
1: ?m.6934
1
,
P: β„• β†’ Prop
P
m: ?m.6925
m
) ↔ (βˆ€
m: ?m.7003
m
< n,
P: β„• β†’ Prop
P
m: ?m.7003
m
) ∧
P: β„• β†’ Prop
P
n :=

Goals accomplished! πŸ™
m, n✝, k: β„•

P: β„• β†’ Prop

n: β„•


(βˆ€ (m : β„•), m < n + 1 β†’ P m) ↔ (βˆ€ (m : β„•), m < n β†’ P m) ∧ P n

Goals accomplished! πŸ™
#align nat.forall_lt_succ
Nat.forall_lt_succ: βˆ€ {P : β„• β†’ Prop} {n : β„•}, (βˆ€ (m : β„•), m < n + 1 β†’ P m) ↔ (βˆ€ (m : β„•), m < n β†’ P m) ∧ P n
Nat.forall_lt_succ
theorem
exists_lt_succ: βˆ€ {P : β„• β†’ Prop} {n : β„•}, (βˆƒ m, m < n + 1 ∧ P m) ↔ (βˆƒ m, m < n ∧ P m) ∨ P n
exists_lt_succ
{
P: β„• β†’ Prop
P
:
β„•: Type
β„•
β†’
Prop: Type
Prop
} {n :
β„•: Type
β„•
} : (βˆƒ
m: ?m.7394
m
< n +
1: ?m.7401
1
,
P: β„• β†’ Prop
P
m: ?m.7394
m
) ↔ (βˆƒ
m: ?m.7471
m
< n,
P: β„• β†’ Prop
P
m: ?m.7471
m
) ∨
P: β„• β†’ Prop
P
n :=

Goals accomplished! πŸ™
m, n✝, k: β„•

P: β„• β†’ Prop

n: β„•


(βˆƒ m, m < n + 1 ∧ P m) ↔ (βˆƒ m, m < n ∧ P m) ∨ P n
m, n✝, k: β„•

P: β„• β†’ Prop

n: β„•


(βˆƒ m, m < n + 1 ∧ P m) ↔ (βˆƒ m, m < n ∧ P m) ∨ P n
m, n✝, k: β„•

P: β„• β†’ Prop

n: β„•


(Β¬βˆƒ m, m < n + 1 ∧ P m) ↔ Β¬((βˆƒ m, m < n ∧ P m) ∨ P n)
m, n✝, k: β„•

P: β„• β†’ Prop

n: β„•


(Β¬βˆƒ m, m < n + 1 ∧ P m) ↔ Β¬((βˆƒ m, m < n ∧ P m) ∨ P n)
m, n✝, k: β„•

P: β„• β†’ Prop

n: β„•


(βˆƒ m, m < n + 1 ∧ P m) ↔ (βˆƒ m, m < n ∧ P m) ∨ P n
m, n✝, k: β„•

P: β„• β†’ Prop

n: β„•


(βˆ€ (m : β„•), m < n + 1 β†’ Β¬P m) ↔ (βˆ€ (m : β„•), m < n β†’ Β¬P m) ∧ Β¬P n
m, n✝, k: β„•

P: β„• β†’ Prop

n: β„•


(βˆƒ m, m < n + 1 ∧ P m) ↔ (βˆƒ m, m < n ∧ P m) ∨ P n

Goals accomplished! πŸ™
#align nat.exists_lt_succ
Nat.exists_lt_succ: βˆ€ {P : β„• β†’ Prop} {n : β„•}, (βˆƒ m, m < n + 1 ∧ P m) ↔ (βˆƒ m, m < n ∧ P m) ∨ P n
Nat.exists_lt_succ
/-! ### `add` -/ -- Sometimes a bare `Nat.add` or similar appears as a consequence of unfolding -- during pattern matching. These lemmas package them back up as typeclass -- mediated operations. @[simp] theorem
add_def: βˆ€ {a b : β„•}, Nat.add a b = a + b
add_def
{a b :
β„•: Type
β„•
} :
Nat.add: β„• β†’ β„• β†’ β„•
Nat.add
a b = a + b :=
rfl: βˆ€ {Ξ± : Sort ?u.7695} {a : Ξ±}, a = a
rfl
#align nat.add_def
Nat.add_def: βˆ€ {a b : β„•}, Nat.add a b = a + b
Nat.add_def
@[simp] theorem
mul_def: βˆ€ {a b : β„•}, Nat.mul a b = a * b
mul_def
{a b :
β„•: Type
β„•
} :
Nat.mul: β„• β†’ β„• β†’ β„•
Nat.mul
a b = a * b :=
rfl: βˆ€ {Ξ± : Sort ?u.7771} {a : Ξ±}, a = a
rfl
#align nat.mul_def
Nat.mul_def: βˆ€ {a b : β„•}, Nat.mul a b = a * b
Nat.mul_def
theorem
exists_eq_add_of_le: m ≀ n β†’ βˆƒ k, n = m + k
exists_eq_add_of_le
(
h: m ≀ n
h
: m ≀ n) : βˆƒ k :
β„•: Type
β„•
, n = m + k := ⟨n - m, (
add_sub_of_le: βˆ€ {a b : β„•}, a ≀ b β†’ a + (b - a) = b
add_sub_of_le
h: m ≀ n
h
).
symm: βˆ€ {Ξ± : Sort ?u.7908} {a b : Ξ±}, a = b β†’ b = a
symm
⟩ #align nat.exists_eq_add_of_le
Nat.exists_eq_add_of_le: βˆ€ {m n : β„•}, m ≀ n β†’ βˆƒ k, n = m + k
Nat.exists_eq_add_of_le
theorem
exists_eq_add_of_le': m ≀ n β†’ βˆƒ k, n = k + m
exists_eq_add_of_le'
(
h: m ≀ n
h
: m ≀ n) : βˆƒ k :
β„•: Type
β„•
, n = k + m := ⟨n - m, (
Nat.sub_add_cancel: βˆ€ {n m : β„•}, m ≀ n β†’ n - m + m = n
Nat.sub_add_cancel
h: m ≀ n
h
).
symm: βˆ€ {Ξ± : Sort ?u.8046} {a b : Ξ±}, a = b β†’ b = a
symm
⟩ #align nat.exists_eq_add_of_le'
Nat.exists_eq_add_of_le': βˆ€ {m n : β„•}, m ≀ n β†’ βˆƒ k, n = k + m
Nat.exists_eq_add_of_le'
theorem
exists_eq_add_of_lt: βˆ€ {m n : β„•}, m < n β†’ βˆƒ k, n = m + k + 1
exists_eq_add_of_lt
(
h: m < n
h
: m < n) : βˆƒ k :
β„•: Type
β„•
, n = m + k +
1: ?m.8088
1
:= ⟨n - (m +
1: ?m.8193
1
),

Goals accomplished! πŸ™
m, n, k: β„•

h: m < n


n = m + (n - (m + 1)) + 1
m, n, k: β„•

h: m < n


n = m + (n - (m + 1)) + 1
m, n, k: β„•

h: m < n


n = m + 1 + (n - (m + 1))
m, n, k: β„•

h: m < n


n = m + (n - (m + 1)) + 1
m, n, k: β„•

h: m < n


n = n

Goals accomplished! πŸ™
⟩ #align nat.exists_eq_add_of_lt
Nat.exists_eq_add_of_lt: βˆ€ {m n : β„•}, m < n β†’ βˆƒ k, n = m + k + 1
Nat.exists_eq_add_of_lt
/-! ### `pred` -/ @[simp] theorem
add_succ_sub_one: βˆ€ (n m : β„•), n + succ m - 1 = n + m
add_succ_sub_one
(n m :
β„•: Type
β„•
) : n +
succ: β„• β†’ β„•
succ
m -
1: ?m.8348
1
= n + m :=

Goals accomplished! πŸ™
m✝, n✝, k, n, m: β„•


n + succ m - 1 = n + m
m✝, n✝, k, n, m: β„•


n + succ m - 1 = n + m
m✝, n✝, k, n, m: β„•


succ (n + m) - 1 = n + m
m✝, n✝, k, n, m: β„•


n + succ m - 1 = n + m
m✝, n✝, k, n, m: β„•


n + m = n + m

Goals accomplished! πŸ™
#align nat.add_succ_sub_one
Nat.add_succ_sub_one: βˆ€ (n m : β„•), n + succ m - 1 = n + m
Nat.add_succ_sub_one
@[simp] theorem
succ_add_sub_one: βˆ€ (n m : β„•), succ n + m - 1 = n + m
succ_add_sub_one
(n m :
β„•: Type
β„•
) :
succ: β„• β†’ β„•
succ
n + m -
1: ?m.8550
1
= n + m :=

Goals accomplished! πŸ™
m✝, n✝, k, n, m: β„•


succ n + m - 1 = n + m
m✝, n✝, k, n, m: β„•


succ n + m - 1 = n + m
m✝, n✝, k, n, m: β„•


succ (n + m) - 1 = n + m
m✝, n✝, k, n, m: β„•


succ n + m - 1 = n + m
m✝, n✝, k, n, m: β„•


n + m = n + m

Goals accomplished! πŸ™
#align nat.succ_add_sub_one
Nat.succ_add_sub_one: βˆ€ (n m : β„•), succ n + m - 1 = n + m
Nat.succ_add_sub_one
theorem
pred_eq_sub_one: βˆ€ (n : β„•), pred n = n - 1
pred_eq_sub_one
(n :
β„•: Type
β„•
) :
pred: β„• β†’ β„•
pred
n = n -
1: ?m.8747
1
:=
rfl: βˆ€ {Ξ± : Sort ?u.8810} {a : Ξ±}, a = a
rfl
#align nat.pred_eq_sub_one
Nat.pred_eq_sub_one: βˆ€ (n : β„•), pred n = n - 1
Nat.pred_eq_sub_one
theorem
pred_eq_of_eq_succ: βˆ€ {m n : β„•}, m = succ n β†’ pred m = n
pred_eq_of_eq_succ
{m n :
β„•: Type
β„•
} (
H: m = succ n
H
: m = n.
succ: β„• β†’ β„•
succ
) : m.
pred: β„• β†’ β„•
pred
= n :=

Goals accomplished! πŸ™
m✝, n✝, k, m, n: β„•

H: m = succ n


pred m = n

Goals accomplished! πŸ™
#align nat.pred_eq_of_eq_succ
Nat.pred_eq_of_eq_succ: βˆ€ {m n : β„•}, m = succ n β†’ pred m = n
Nat.pred_eq_of_eq_succ
@[simp] theorem
pred_eq_succ_iff: βˆ€ {n m : β„•}, pred n = succ m ↔ n = m + 2
pred_eq_succ_iff
{n m :
β„•: Type
β„•
} :
pred: β„• β†’ β„•
pred
n =
succ: β„• β†’ β„•
succ
m ↔ n = m +
2: ?m.8954
2
:=

Goals accomplished! πŸ™
m✝, n✝, k, n, m: β„•


pred n = succ m ↔ n = m + 2
m✝, n, k, m: β„•


zero
m✝, n, k, m, n✝: β„•


succ
pred (succ n✝) = succ m ↔ succ n✝ = m + 2
m✝, n✝, k, n, m: β„•


pred n = succ m ↔ n = m + 2
m✝, n, k, m: β„•


zero
m✝, n, k, m, n✝: β„•


succ
pred (succ n✝) = succ m ↔ succ n✝ = m + 2
m✝, n✝, k, n, m: β„•


pred n = succ m ↔ n = m + 2
m✝, n, k, m, n✝: β„•


succ.mp
pred (succ n✝) = succ m β†’ succ n✝ = m + 2
m✝, n, k, m, n✝: β„•


succ.mpr
succ n✝ = m + 2 β†’ pred (succ n✝) = succ m
m✝, n✝, k, n, m: β„•


pred n = succ m ↔ n = m + 2
m✝, n, k, m: β„•


zero.mp
pred zero = succ m β†’ zero = m + 2
m✝, n, k, m: β„•


zero.mpr
zero = m + 2 β†’ pred zero = succ m
m✝, n, k, m, n✝: β„•


succ.mp
pred (succ n✝) = succ m β†’ succ n✝ = m + 2
m✝, n, k, m, n✝: β„•


succ.mpr
succ n✝ = m + 2 β†’ pred (succ n✝) = succ m
m✝, n✝, k, n, m: β„•


pred n = succ m ↔ n = m + 2

Goals accomplished! πŸ™
m✝, n✝, k, n, m: β„•


pred n = succ m ↔ n = m + 2
m✝, n, k, m: β„•


succ.mp.refl
succ (succ m) = m + 2
m✝, n, k, m: β„•


succ.mpr.refl
pred (succ (Nat.add m 1)) = succ m
m✝, n✝, k, n, m: β„•


pred n = succ m ↔ n = m + 2

Goals accomplished! πŸ™
#align nat.pred_eq_succ_iff
Nat.pred_eq_succ_iff: βˆ€ {n m : β„•}, pred n = succ m ↔ n = m + 2
Nat.pred_eq_succ_iff
theorem
pred_sub: βˆ€ (n m : β„•), pred n - m = pred (n - m)
pred_sub
(n m :
β„•: Type
β„•
) :
pred: β„• β†’ β„•
pred
n - m =
pred: β„• β†’ β„•
pred
(n - m) :=

Goals accomplished! πŸ™
m✝, n✝, k, n, m: β„•


pred n - m = pred (n - m)
m✝, n✝, k, n, m: β„•


pred n - m = pred (n - m)
m✝, n✝, k, n, m: β„•


n - 1 - m = pred (n - m)
m✝, n✝, k, n, m: β„•


pred n - m = pred (n - m)
m✝, n✝, k, n, m: β„•


n - (1 + m) = pred (n - m)
m✝, n✝, k, n, m: β„•


pred n - m = pred (n - m)
m✝, n✝, k, n, m: β„•


n - succ m = pred (n - m)
m✝, n✝, k, n, m: β„•


pred n - m = pred (n - m)
m✝, n✝, k, n, m: β„•


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

Goals accomplished! πŸ™
#align nat.pred_sub
Nat.pred_sub: βˆ€ (n m : β„•), pred n - m = pred (n - m)
Nat.pred_sub
-- Moved to Std #align nat.le_pred_of_lt
Nat.le_pred_of_lt: βˆ€ {m n : β„•}, m < n β†’ m ≀ n - 1
Nat.le_pred_of_lt
theorem
le_of_pred_lt: βˆ€ {m n : β„•}, pred m < n β†’ m ≀ n
le_of_pred_lt
{m n :
β„•: Type
β„•
} :
pred: β„• β†’ β„•
pred
m < n β†’ m ≀ n := match m with | 0 =>
le_of_lt: βˆ€ {Ξ± : Type ?u.9620} [inst : Preorder Ξ±] {a b : Ξ±}, a < b β†’ a ≀ b
le_of_lt
| _ + 1 =>
id: βˆ€ {Ξ± : Sort ?u.9749}, Ξ± β†’ Ξ±
id
#align nat.le_of_pred_lt
Nat.le_of_pred_lt: βˆ€ {m n : β„•}, pred m < n β†’ m ≀ n
Nat.le_of_pred_lt
/-- This ensures that `simp` succeeds on `pred (n + 1) = n`. -/ @[simp] theorem
pred_one_add: βˆ€ (n : β„•), pred (1 + n) = n
pred_one_add
(n :
β„•: Type
β„•
) :
pred: β„• β†’ β„•
pred
(
1: ?m.9843
1
+ n) = n :=

Goals accomplished! πŸ™
m, n✝, k, n: β„•


pred (1 + n) = n
m, n✝, k, n: β„•


pred (1 + n) = n
m, n✝, k, n: β„•


pred (n + 1) = n
m, n✝, k, n: β„•


pred (1 + n) = n
m, n✝, k, n: β„•


pred (succ n) = n
m, n✝, k, n: β„•


pred (1 + n) = n
m, n✝, k, n: β„•


n = n

Goals accomplished! πŸ™
#align nat.pred_one_add
Nat.pred_one_add: βˆ€ (n : β„•), pred (1 + n) = n
Nat.pred_one_add
/-! ### `mul` -/ theorem
two_mul_ne_two_mul_add_one: βˆ€ {n m : β„•}, 2 * n β‰  2 * m + 1
two_mul_ne_two_mul_add_one
{
n: ?m.9988
n
m: ?m.9991
m
} :
2: ?m.10000
2
*
n: ?m.9988
n
β‰ 
2: ?m.10033
2
*
m: ?m.9991
m
+
1: ?m.10043
1
:=
mt: βˆ€ {a b : Prop}, (a β†’ b) β†’ Β¬b β†’ Β¬a
mt
(
congr_arg: βˆ€ {Ξ± : Sort ?u.10389} {Ξ² : Sort ?u.10388} {a₁ aβ‚‚ : Ξ±} (f : Ξ± β†’ Ξ²), a₁ = aβ‚‚ β†’ f a₁ = f aβ‚‚
congr_arg
(Β· % 2): β„• β†’ β„•
(Β· % 2)
) (

Goals accomplished! πŸ™
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = (2 * m + 1) % 2
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = (2 * m + 1) % 2
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = (1 + 2 * m) % 2
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = (2 * m + 1) % 2
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = 1 % 2
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = (2 * m + 1) % 2
m✝, n✝, k, n, m: β„•


Β¬0 = 1 % 2
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = (2 * m + 1) % 2
m✝, n✝, k, n, m: β„•


Β¬0 = 1
m✝, n✝, k, n, m: β„•


1 < 2
m✝, n✝, k, n, m: β„•


Β¬0 = 1
m✝, n✝, k, n, m: β„•


1 < 2
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = (2 * m + 1) % 2
m✝, n✝, k, n, m: β„•


Β¬0 = 1
m✝, n✝, k, n, m: β„•


1 < 2
m✝, n✝, k, n, m: β„•


Β¬2 * n % 2 = (2 * m + 1) % 2

Goals accomplished! πŸ™
) #align nat.two_mul_ne_two_mul_add_one
Nat.two_mul_ne_two_mul_add_one: βˆ€ {n m : β„•}, 2 * n β‰  2 * m + 1
Nat.two_mul_ne_two_mul_add_one
theorem
mul_ne_mul_left: βˆ€ {a b c : β„•}, 0 < a β†’ (b * a β‰  c * a ↔ b β‰  c)
mul_ne_mul_left
{a b c :
β„•: Type
β„•
} (
ha: 0 < a
ha
:
0: ?m.10686
0
< a) : b * a β‰  c * a ↔ b β‰  c := (
mul_left_injectiveβ‚€: βˆ€ {Mβ‚€ : Type ?u.10803} [inst : Mul Mβ‚€] [inst_1 : Zero Mβ‚€] [inst_2 : IsRightCancelMulZero Mβ‚€] {b : Mβ‚€}, b β‰  0 β†’ Function.Injective fun a => a * b
mul_left_injectiveβ‚€
ha: 0 < a
ha
.
ne': βˆ€ {Ξ± : Type ?u.10809} [inst : Preorder Ξ±] {x y : Ξ±}, x < y β†’ y β‰  x
ne'
).
ne_iff: βˆ€ {Ξ± : Sort ?u.10931} {Ξ² : Sort ?u.10932} {f : Ξ± β†’ Ξ²}, Function.Injective f β†’ βˆ€ {x y : Ξ±}, f x β‰  f y ↔ x β‰  y
ne_iff
#align nat.mul_ne_mul_left
Nat.mul_ne_mul_left: βˆ€ {a b c : β„•}, 0 < a β†’ (b * a β‰  c * a ↔ b β‰  c)
Nat.mul_ne_mul_left
theorem
mul_ne_mul_right: βˆ€ {a b c : β„•}, 0 < a β†’ (a * b β‰  a * c ↔ b β‰  c)
mul_ne_mul_right
{a b c :
β„•: Type
β„•
} (
ha: 0 < a
ha
:
0: ?m.10978
0
< a) : a * b β‰  a * c ↔ b β‰  c := (
mul_right_injectiveβ‚€: βˆ€ {Mβ‚€ : Type ?u.11095} [inst : Mul Mβ‚€] [inst_1 : Zero Mβ‚€] [inst_2 : IsLeftCancelMulZero Mβ‚€] {a : Mβ‚€}, a β‰  0 β†’ Function.Injective ((fun x x_1 => x * x_1) a)
mul_right_injectiveβ‚€
ha: 0 < a
ha
.
ne': βˆ€ {Ξ± : Type ?u.11101} [inst : Preorder Ξ±] {x y : Ξ±}, x < y β†’ y β‰  x
ne'
).
ne_iff: βˆ€ {Ξ± : Sort ?u.11190} {Ξ² : Sort ?u.11191} {f : Ξ± β†’ Ξ²}, Function.Injective f β†’ βˆ€ {x y : Ξ±}, f x β‰  f y ↔ x β‰  y
ne_iff
#align nat.mul_ne_mul_right
Nat.mul_ne_mul_right: βˆ€ {a b c : β„•}, 0 < a β†’ (a * b β‰  a * c ↔ b β‰  c)
Nat.mul_ne_mul_right
theorem
mul_right_eq_self_iff: βˆ€ {a b : β„•}, 0 < a β†’ (a * b = a ↔ b = 1)
mul_right_eq_self_iff
{a b :
β„•: Type
β„•
} (
ha: 0 < a
ha
:
0: ?m.11237
0
< a) : a * b = a ↔ b =
1: ?m.11322
1
:= suffices a * b = a *
1: ?m.11355
1
↔ b =
1: ?m.11421
1
by
m, n, k, a, b: β„•

ha: 0 < a

this: a * b = a * 1 ↔ b = 1


a * b = a ↔ b = 1
m, n, k, a, b: β„•

ha: 0 < a

this: a * b = a ↔ b = 1


a * b = a ↔ b = 1
m, n, k, a, b: β„•

ha: 0 < a

this: a * b = a ↔ b = 1


a * b = a ↔ b = 1

Goals accomplished! πŸ™
mul_right_inj': βˆ€ {Mβ‚€ : Type ?u.11437} [inst : CancelMonoidWithZero Mβ‚€] {a b c : Mβ‚€}, a β‰  0 β†’ (a * b = a * c ↔ b = c)
mul_right_inj'
ha: 0 < a
ha
.
ne': βˆ€ {Ξ± : Type ?u.11474} [inst : Preorder Ξ±] {x y : Ξ±}, x < y β†’ y β‰  x
ne'
#align nat.mul_right_eq_self_iff
Nat.mul_right_eq_self_iff: βˆ€ {a b : β„•}, 0 < a β†’ (a * b = a ↔ b = 1)
Nat.mul_right_eq_self_iff
theorem
mul_left_eq_self_iff: βˆ€ {a b : β„•}, 0 < b β†’ (a * b = b ↔ a = 1)
mul_left_eq_self_iff
{a b :
β„•: Type
β„•
} (
hb: 0 < b
hb
:
0: ?m.11619
0
< b) : a * b = b ↔ a =
1: ?m.11704
1
:=

Goals accomplished! πŸ™
m, n, k, a, b: β„•

hb: 0 < b


a * b = b ↔ a = 1
m, n, k, a, b: β„•

hb: 0 < b


a * b = b ↔ a = 1
m, n, k, a, b: β„•

hb: 0 < b


b * a = b ↔ a = 1
m, n, k, a, b: β„•

hb: 0 < b


a * b = b ↔ a = 1
m, n, k, a, b: β„•

hb: 0 < b


a = 1 ↔ a = 1

Goals accomplished! πŸ™
#align nat.mul_left_eq_self_iff
Nat.mul_left_eq_self_iff: βˆ€ {a b : β„•}, 0 < b β†’ (a * b = b ↔ a = 1)
Nat.mul_left_eq_self_iff
theorem
lt_succ_iff_lt_or_eq: βˆ€ {n i : β„•}, n < succ i ↔ n < i ∨ n = i
lt_succ_iff_lt_or_eq
{n i :
β„•: Type
β„•
} : n < i.
succ: β„• β†’ β„•
succ
↔ n < i ∨ n = i :=
lt_succ_iff: βˆ€ {m n : β„•}, m < succ n ↔ m ≀ n
lt_succ_iff
.
trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
trans
Decidable.le_iff_lt_or_eq: βˆ€ {Ξ± : Type ?u.11834} [inst : PartialOrder Ξ±] [inst_1 : DecidableRel fun x x_1 => x ≀ x_1] {a b : Ξ±}, a ≀ b ↔ a < b ∨ a = b
Decidable.le_iff_lt_or_eq
#align nat.lt_succ_iff_lt_or_eq
Nat.lt_succ_iff_lt_or_eq: βˆ€ {n i : β„•}, n < succ i ↔ n < i ∨ n = i
Nat.lt_succ_iff_lt_or_eq
/-! ### 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. -/ -- Porting note: The type ascriptions of these two theorems need to be changed, -- as mathport wrote a lambda that wasn't there in mathlib3, that prevents `simp` applying them. @[simp] theorem
rec_zero: βˆ€ {C : β„• β†’ Sort u} (h0 : C 0) (h : (n : β„•) β†’ C n β†’ C (n + 1)), rec h0 h 0 = h0
rec_zero
{
C: β„• β†’ Sort u
C
:
β„•: Type
β„•
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} (
h0: C 0
h0
:
C: β„• β†’ Sort u
C
0: ?m.11942
0
) (
h: (n : β„•) β†’ C n β†’ C (n + 1)
h
: βˆ€
n: ?m.11955
n
,
C: β„• β†’ Sort u
C
n: ?m.11955
n
β†’
C: β„• β†’ Sort u
C
(
n: ?m.11955
n
+
1: ?m.11964
1
)) :
Nat.rec: {motive : β„• β†’ Sort ?u.12061} β†’ motive zero β†’ ((n : β„•) β†’ motive n β†’ motive (succ n)) β†’ (t : β„•) β†’ motive t
Nat.rec
h0: C 0
h0
h: (n : β„•) β†’ C n β†’ C (n + 1)
h
0: ?m.12081
0
=
h0: C 0
h0
:=
rfl: βˆ€ {Ξ± : Sort ?u.12119} {a : Ξ±}, a = a
rfl
#align nat.rec_zero
Nat.rec_zero: βˆ€ {C : β„• β†’ Sort u} (h0 : C 0) (h : (n : β„•) β†’ C n β†’ C (n + 1)), rec h0 h 0 = h0
Nat.rec_zero
@[simp] theorem
rec_add_one: βˆ€ {C : β„• β†’ Sort u} (h0 : C 0) (h : (n : β„•) β†’ C n β†’ C (n + 1)) (n : β„•), rec h0 h (n + 1) = h n (rec h0 h n)
rec_add_one
{
C: β„• β†’ Sort u
C
:
β„•: Type
β„•
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} (
h0: C 0
h0
:
C: β„• β†’ Sort u
C
0: ?m.12160
0
) (
h: (n : β„•) β†’ C n β†’ C (n + 1)
h
: βˆ€
n: ?m.12173
n
,
C: β„• β†’ Sort u
C
n: ?m.12173
n
β†’
C: β„• β†’ Sort u
C
(
n: ?m.12173
n
+
1: ?m.12182
1
)) (n :
β„•: Type
β„•
) :
Nat.rec: {motive : β„• β†’ Sort ?u.12340} β†’ motive zero β†’ ((n : β„•) β†’ motive n β†’ motive (succ n)) β†’ (t : β„•) β†’ motive t
Nat.rec
h0: C 0
h0
h: (n : β„•) β†’ C n β†’ C (n + 1)
h
(n +
1: ?m.12363
1
) =
h: (n : β„•) β†’ C n β†’ C (n + 1)
h
n (
Nat.rec: {motive : β„• β†’ Sort ?u.12267} β†’ motive zero β†’ ((n : β„•) β†’ motive n β†’ motive (succ n)) β†’ (t : β„•) β†’ motive t
Nat.rec
h0: C 0
h0
h: (n : β„•) β†’ C n β†’ C (n + 1)
h
n) :=
rfl: βˆ€ {Ξ± : Sort ?u.12429} {a : Ξ±}, a = a
rfl
#align nat.rec_add_one
Nat.rec_add_one: βˆ€ {C : β„• β†’ Sort u} (h0 : C 0) (h : (n : β„•) β†’ C n β†’ C (n + 1)) (n : β„•), rec h0 h (n + 1) = h n (rec h0 h n)
Nat.rec_add_one
/-- 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 `leRecOn`. -/ @[elab_as_elim] def
leRecOn: {C : β„• β†’ Sort u} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
{
C: β„• β†’ Sort u
C
:
β„•: Type
β„•
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {n :
β„•: Type
β„•
} : βˆ€ {m :
β„•: Type
β„•
}, n ≀ m β†’ (βˆ€ {
k: ?m.12508
k
},
C: β„• β†’ Sort u
C
k: ?m.12508
k
β†’
C: β„• β†’ Sort u
C
(
k: ?m.12508
k
+
1: ?m.12517
1
)) β†’
C: β„• β†’ Sort u
C
n β†’
C: β„• β†’ Sort u
C
m | 0,
H: n ≀ 0
H
, _,
x: C n
x
=>
Eq.recOn: {Ξ± : Sort ?u.12643} β†’ {a : Ξ±} β†’ {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.12644} β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a (_ : a = a) β†’ motive a_1 t
Eq.recOn
(
Nat.eq_zero_of_le_zero: βˆ€ {n : β„•}, n ≀ 0 β†’ n = 0
Nat.eq_zero_of_le_zero
H: n ≀ 0
H
)
x: C n
x
| m + 1,
H: n ≀ m + 1
H
,
next: {k : β„•} β†’ C k β†’ C (k + 1)
next
,
x: C n
x
=>
Or.by_cases: {p q : Prop} β†’ [inst : Decidable p] β†’ {Ξ± : Sort ?u.12773} β†’ p ∨ q β†’ (p β†’ Ξ±) β†’ (q β†’ Ξ±) β†’ Ξ±
Or.by_cases
(
of_le_succ: βˆ€ {n m : β„•}, n ≀ succ m β†’ n ≀ m ∨ n = succ m
of_le_succ
H: n ≀ m + 1
H
) (fun
h: n ≀ m
h
: n ≀ m =>
next: {k : β„•} β†’ C k β†’ C (k + 1)
next
<|
leRecOn: {C : β„• β†’ Sort u} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
h: n ≀ m
h
(@
next: {k : β„•} β†’ C k β†’ C (k + 1)
next
)
x: C n
x
) fun
h: n = m + 1
h
: n = m +
1: ?m.12884
1
=>
Eq.recOn: {Ξ± : Sort ?u.12922} β†’ {a : Ξ±} β†’ {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.12923} β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a (_ : a = a) β†’ motive a_1 t
Eq.recOn
h: n = m + 1
h
x: C n
x
#align nat.le_rec_on
Nat.leRecOn: {C : β„• β†’ Sort u} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
Nat.leRecOn
theorem
leRecOn_self: βˆ€ {C : β„• β†’ Sort u} {n : β„•} {h : n ≀ n} {next : {k : β„•} β†’ C k β†’ C (k + 1)} (x : C n), leRecOn h (fun {k} => next) x = x
leRecOn_self
{
C: β„• β†’ Sort u
C
:
β„•: Type
β„•
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {
n: ?m.13782
n
} {
h: n ≀ n
h
:
n: ?m.13782
n
≀
n: ?m.13782
n
} {
next: {k : β„•} β†’ C k β†’ C (k + 1)
next
: βˆ€ {
k: ?m.13826
k
},
C: β„• β†’ Sort u
C
k: ?m.13826
k
β†’
C: β„• β†’ Sort u
C
(
k: ?m.13826
k
+
1: ?m.13835
1
)} (
x: C n
x
:
C: β„• β†’ Sort u
C
n: ?m.13782
n
) : (
leRecOn: {C : β„• β†’ Sort ?u.13905} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
h: n ≀ n
h
next: {k : β„•} β†’ C k β†’ C (k + 1)
next
x: C n
x
:
C: β„• β†’ Sort u
C
n: ?m.13782
n
) =
x: C n
x
:=

Goals accomplished! πŸ™
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h (fun {k} => next) x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

h: zero ≀ zero

x: C zero


zero
leRecOn h (fun {k} => next) x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
leRecOn h (fun {k} => next) x = x
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h (fun {k} => next) x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

h: zero ≀ zero

x: C zero


zero
leRecOn h (fun {k} => next) x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
leRecOn h (fun {k} => next) x = x
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h (fun {k} => next) x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
(Or.by_cases (_ : succ n✝ ≀ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) fun h => h β–Έ x) = x
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h (fun {k} => next) x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

h: zero ≀ zero

x: C zero


zero
(_ : zero = 0) β–Έ x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

h: zero ≀ zero

x: C zero


zero
(_ : zero = 0) β–Έ x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
(Or.by_cases (_ : succ n✝ ≀ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) fun h => h β–Έ x) = x

Goals accomplished! πŸ™
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h (fun {k} => next) x = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
(Or.by_cases (_ : succ n✝ ≀ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) fun h => h β–Έ x) = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
(Or.by_cases (_ : succ n✝ ≀ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) fun h => h β–Έ x) = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
(if hp : succ n✝ ≀ n✝ then (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) hp else (fun h => h β–Έ x) (_ : succ n✝ = succ n✝)) = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
(Or.by_cases (_ : succ n✝ ≀ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) fun h => h β–Έ x) = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
(if hp : succ n✝ ≀ n✝ then (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) hp else (fun h => h β–Έ x) (_ : succ n✝ = succ n✝)) = x
m, n, k: β„•

C: β„• β†’ Sort u

next: {k : β„•} β†’ C k β†’ C (k + 1)

n✝: β„•

h: succ n✝ ≀ succ n✝

x: C (succ n✝)


succ
(fun h => h β–Έ x) (_ : succ n✝ = succ n✝) = x

Goals accomplished! πŸ™
#align nat.le_rec_on_self
Nat.leRecOn_self: βˆ€ {C : β„• β†’ Sort u} {n : β„•} {h : n ≀ n} {next : {k : β„•} β†’ C k β†’ C (k + 1)} (x : C n), leRecOn h (fun {k} => next) x = x
Nat.leRecOn_self
theorem
leRecOn_succ: βˆ€ {C : β„• β†’ Sort u} {n m : β„•} (h1 : n ≀ m) {h2 : n ≀ m + 1} {next : {k : β„•} β†’ C k β†’ C (k + 1)} (x : C n), leRecOn h2 next x = next (leRecOn h1 next x)
leRecOn_succ
{
C: β„• β†’ Sort u
C
:
β„•: Type
β„•
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {
n: ?m.15988
n
m} (
h1: n ≀ m
h1
:
n: ?m.15988
n
≀
m: ?m.15991
m
) {
h2: n ≀ m + 1
h2
:
n: ?m.15988
n
≀
m: ?m.15991
m
+
1: ?m.16039
1
} {
next: ?m.16117
next
} (
x: C n
x
:
C: β„• β†’ Sort u
C
n: ?m.15988
n
) : (
leRecOn: {C : β„• β†’ Sort ?u.16188} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
h2: n ≀ m + 1
h2
(@
next: ?m.16117
next
)
x: C n
x
:
C: β„• β†’ Sort u
C
(
m: ?m.15991
m
+
1: ?m.16128
1
)) =
next: ?m.16117
next
(
leRecOn: {C : β„• β†’ Sort ?u.16236} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
h1: n ≀ m
h1
(@
next: ?m.16117
next
)
x: C n
x
:
C: β„• β†’ Sort u
C
m: ?m.15991
m
) :=

Goals accomplished! πŸ™
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h2 next x = next (leRecOn h1 next x)
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


next (leRecOn h1 next x)
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h2 next x = next (leRecOn h1 next x)
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h2 next x
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h2 next x = next (leRecOn h1 next x)
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h2 next x
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


Or.by_cases (_ : n ≀ m ∨ n = succ m) (fun h => next (leRecOn h next x)) fun h => Eq.recOn h x
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h2 next x
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


if hp : n ≀ m then next (leRecOn hp next x) else Eq.recOn (_ : n = succ m) x
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h2 next x
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


next (leRecOn h1 next x)
m✝, n✝, k: β„•

C: β„• β†’ Sort u

n, m: β„•

h1: n ≀ m

h2: n ≀ m + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


next (leRecOn h1 next x)
#align nat.le_rec_on_succ
Nat.leRecOn_succ: βˆ€ {C : β„• β†’ Sort u} {n m : β„•} (h1 : n ≀ m) {h2 : n ≀ m + 1} {next : {k : β„•} β†’ C k β†’ C (k + 1)} (x : C n), leRecOn h2 next x = next (leRecOn h1 next x)
Nat.leRecOn_succ
theorem
leRecOn_succ': βˆ€ {C : β„• β†’ Sort u} {n : β„•} {h : n ≀ n + 1} {next : {k : β„•} β†’ C k β†’ C (k + 1)} (x : C n), leRecOn h (fun {k} => next) x = next x
leRecOn_succ'
{
C: β„• β†’ Sort u
C
:
β„•: Type
β„•
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {
n: ?m.16660
n
} {
h: n ≀ n + 1
h
:
n: ?m.16660
n
≀
n: ?m.16660
n
+
1: ?m.16668
1
} {
next: {k : β„•} β†’ C k β†’ C (k + 1)
next
: βˆ€ {
k: ?m.16747
k
},
C: β„• β†’ Sort u
C
k: ?m.16747
k
β†’
C: β„• β†’ Sort u
C
(
k: ?m.16747
k
+
1: ?m.16756
1
)} (
x: C n
x
:
C: β„• β†’ Sort u
C
n: ?m.16660
n
) : (
leRecOn: {C : β„• β†’ Sort ?u.16882} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
h: n ≀ n + 1
h
next: {k : β„•} β†’ C k β†’ C (k + 1)
next
x: C n
x
:
C: β„• β†’ Sort u
C
(
n: ?m.16660
n
+
1: ?m.16838
1
)) =
next: {k : β„•} β†’ C k β†’ C (k + 1)
next
x: C n
x
:=

Goals accomplished! πŸ™
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h (fun {k} => next) x = next x
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h (fun {k} => next) x = next x
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


next (leRecOn (_ : n ≀ n) (fun {k} => next) x) = next x
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn h (fun {k} => next) x = next x
m, n✝, k: β„•

C: β„• β†’ Sort u

n: β„•

h: n ≀ n + 1

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


next x = next x

Goals accomplished! πŸ™
#align nat.le_rec_on_succ'
Nat.leRecOn_succ': βˆ€ {C : β„• β†’ Sort u} {n : β„•} {h : n ≀ n + 1} {next : {k : β„•} β†’ C k β†’ C (k + 1)} (x : C n), leRecOn h (fun {k} => next) x = next x
Nat.leRecOn_succ'
theorem
leRecOn_trans: βˆ€ {C : β„• β†’ Sort u} {n m k : β„•} (hnm : n ≀ m) (hmk : m ≀ k) {next : {k : β„•} β†’ C k β†’ C (k + 1)} (x : C n), leRecOn (_ : n ≀ k) next x = leRecOn hmk next (leRecOn hnm next x)
leRecOn_trans
{
C: β„• β†’ Sort u
C
:
β„•: Type
β„•
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {
n: ?m.17052
n
m: ?m.17055
m
k} (
hnm: n ≀ m
hnm
:
n: ?m.17052
n
≀
m: ?m.17055
m
) (
hmk: m ≀ k
hmk
:
m: ?m.17055
m
≀
k: ?m.17058
k
) {
next: ?m.17141
next
} (
x: C n
x
:
C: β„• β†’ Sort u
C
n: ?m.17052
n
) : (
leRecOn: {C : β„• β†’ Sort ?u.17148} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
(
le_trans: βˆ€ {Ξ± : Type ?u.17173} [inst : Preorder Ξ±] {a b c : Ξ±}, a ≀ b β†’ b ≀ c β†’ a ≀ c
le_trans
hnm: n ≀ m
hnm
hmk: m ≀ k
hmk
) (@
next: ?m.17141
next
)
x: C n
x
:
C: β„• β†’ Sort u
C
k: ?m.17058
k
) =
leRecOn: {C : β„• β†’ Sort ?u.17251} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
hmk: m ≀ k
hmk
(@
next: ?m.17141
next
) (
leRecOn: {C : β„• β†’ Sort ?u.17280} β†’ {n m : β„•} β†’ n ≀ m β†’ ({k : β„•} β†’ C k β†’ C (k + 1)) β†’ C n β†’ C m
leRecOn
hnm: n ≀ m
hnm
(@
next: ?m.17141
next
)
x: C n
x
) :=

Goals accomplished! πŸ™
m✝, n✝, k✝: β„•

C: β„• β†’ Sort u

n, m, k: β„•

hnm: n ≀ m

hmk: m ≀ k

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn (_ : n ≀ k) next x = leRecOn hmk next (leRecOn hnm next x)
m✝, n✝, k✝: β„•

C: β„• β†’ Sort u

n, m, k: β„•

hnm: n ≀ m

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


refl
leRecOn (_ : n ≀ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
m✝, n✝, k✝¹: β„•

C: β„• β†’ Sort u

n, m, k✝: β„•

hnm: n ≀ m

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n

k: β„•

hmk: Nat.le m k

ih: leRecOn (_ : n ≀ k) next x = leRecOn hmk next (leRecOn hnm next x)


step
leRecOn (_ : n ≀ succ k) next x = leRecOn (_ : Nat.le m (succ k)) next (leRecOn hnm next x)
m✝, n✝, k✝: β„•

C: β„• β†’ Sort u

n, m, k: β„•

hnm: n ≀ m

hmk: m ≀ k

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn (_ : n ≀ k) next x = leRecOn hmk next (leRecOn hnm next x)
m✝, n✝, k✝: β„•

C: β„• β†’ Sort u

n, m, k: β„•

hnm: n ≀ m

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


refl
leRecOn (_ : n ≀ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
m✝, n✝, k✝: β„•

C: β„• β†’ Sort u

n, m, k: β„•

hnm: n ≀ m

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


refl
leRecOn (_ : n ≀ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
m✝, n✝, k✝¹: β„•

C: β„• β†’ Sort u

n, m, k✝: β„•

hnm: n ≀ m

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n

k: β„•

hmk: Nat.le m k

ih: leRecOn (_ : n ≀ k) next x = leRecOn hmk next (leRecOn hnm next x)


step
leRecOn (_ : n ≀ succ k) next x = leRecOn (_ : Nat.le m (succ k)) next (leRecOn hnm next x)
m✝, n✝, k✝: β„•

C: β„• β†’ Sort u

n, m, k: β„•

hnm: n ≀ m

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


refl
leRecOn (_ : n ≀ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
m✝, n✝, k✝: β„•

C: β„• β†’ Sort u

n, m, k: β„•

hnm: n ≀ m

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


refl
leRecOn (_ : n ≀ m) next x = leRecOn hnm next x

Goals accomplished! πŸ™
m✝, n✝, k✝: β„•

C: β„• β†’ Sort u

n, m, k: β„•

hnm: n ≀ m

hmk: m ≀ k

next: {k : β„•} β†’ C k β†’ C (k + 1)

x: C n


leRecOn (_ : n ≀ k) next x = leRecOn hmk next (leRecOn hnm next x)
m✝, n✝, k✝¹: β„•

C: β„• β†’ Sort u

n, m, k✝: β„•

hnm: n