rec/cases

@[simp]

theorem Nat.recAux_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) : Nat.recAux zero succ 0 = zero

theorem Nat.recAux_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (n : Nat) : Nat.recAux zero succ (n + 1) = succ n (Nat.recAux zero succ n)

@[simp]

theorem Nat.recAuxOn_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) : Nat.recAuxOn 0 zero succ = zero

theorem Nat.recAuxOn_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (n : Nat) : Nat.recAuxOn (n + 1) zero succ = succ n (Nat.recAuxOn n zero succ)

@[simp]

theorem Nat.casesAuxOn_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) : Nat.casesAuxOn 0 zero succ = zero

@[simp]

theorem Nat.casesAuxOn_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) (n : Nat) : Nat.casesAuxOn (n + 1) zero succ = succ n

theorem Nat.strongRec_eq {motive : Nat → Sort u_1} (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) (t : Nat) : Nat.strongRec ind t = ind t fun m x => Nat.strongRec ind m

theorem Nat.strongRecOn_eq {motive : Nat → Sort u_1} (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) (t : Nat) : Nat.strongRecOn t ind = ind t fun m x => Nat.strongRecOn m ind

@[simp]

theorem Nat.recDiagAux_zero_left {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiagAux zero_left zero_right succ_succ 0 n = zero_left n

@[simp]

theorem Nat.recDiagAux_zero_right {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (h : autoParam (zero_left 0 = zero_right 0) _auto✝) : Nat.recDiagAux zero_left zero_right succ_succ m 0 = zero_right m

theorem Nat.recDiagAux_succ_succ {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : Nat.recDiagAux zero_left zero_right succ_succ (m + 1) (n + 1) = succ_succ m n (Nat.recDiagAux zero_left zero_right succ_succ m n)

@[simp]

theorem Nat.recDiag_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 0 = zero_zero

theorem Nat.recDiag_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 (n + 1) = zero_succ n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 n)

theorem Nat.recDiag_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) 0 = succ_zero m (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m 0)

theorem Nat.recDiag_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) (n + 1) = succ_succ m n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n)

@[simp]

theorem Nat.recDiagOn_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) : Nat.recDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero

theorem Nat.recDiagOn_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n (Nat.recDiagOn 0 n zero_zero zero_succ succ_zero succ_succ)

theorem Nat.recDiagOn_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) : Nat.recDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m (Nat.recDiagOn m 0 zero_zero zero_succ succ_zero succ_succ)

theorem Nat.recDiagOn_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : Nat.recDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n (Nat.recDiagOn m n zero_zero zero_succ succ_zero succ_succ)

@[simp]

theorem Nat.casesDiagOn_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) : Nat.casesDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero

@[simp]

theorem Nat.casesDiagOn_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (n : Nat) : Nat.casesDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n

@[simp]

theorem Nat.casesDiagOn_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (m : Nat) : Nat.casesDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m

@[simp]

theorem Nat.casesDiagOn_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : Nat.casesDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n

le/lt

theorem Nat.ne_of_gt {a : Nat} {b : Nat} (h : b < a) : a ≠ b

theorem Nat.le_of_not_le {a : Nat} {b : Nat} : ¬a ≤ b → b ≤ a

theorem Nat.lt_iff_le_not_le {m : Nat} {n : Nat} : m < n ↔ m ≤ n ∧ ¬n ≤ m

theorem Nat.lt_iff_le_and_ne {m : Nat} {n : Nat} : m < n ↔ m ≤ n ∧ m ≠ n

@[simp]

theorem Nat.not_le {a : Nat} {b : Nat} : ¬a ≤ b ↔ b < a

@[simp]

theorem Nat.not_lt {a : Nat} {b : Nat} : ¬a < b ↔ b ≤ a

theorem Nat.le_lt_antisymm {n : Nat} {m : Nat} (h₁ : n ≤ m) (h₂ : m < n) : False

theorem Nat.lt_le_antisymm {n : Nat} {m : Nat} (h₁ : n < m) (h₂ : m ≤ n) : False

theorem Nat.lt_asymm {n : Nat} {m : Nat} (h₁ : n < m) : ¬m < n

def Nat.lt_sum_ge (a : Nat) (b : Nat) : a < b ⊕' b ≤ a

Strong case analysis on a < b ∨ b ≤ a

Equations

• Nat.lt_sum_ge a b = if h : a < b then PSum.inl h else PSum.inr (_ : b ≤ a)

def Nat.sum_trichotomy (a : Nat) (b : Nat) : a < b ⊕' a = b ⊕' b < a

Strong case analysis on a < b ∨ a = b ∨ b < a

Equations

• One or more equations did not get rendered due to their size.

theorem Nat.lt_trichotomy (a : Nat) (b : Nat) : a < b ∨ a = b ∨ b < a

theorem Nat.eq_or_lt_of_not_lt {a : Nat} {b : Nat} (hnlt : ¬a < b) : a = b ∨ b < a

theorem Nat.not_lt_of_le {n : Nat} {m : Nat} (h₁ : m ≤ n) : ¬n < m

theorem Nat.not_le_of_lt {n : Nat} {m : Nat} : m < n → ¬n ≤ m

theorem Nat.lt_of_not_le {a : Nat} {b : Nat} : ¬a ≤ b → b < a

theorem Nat.le_of_not_lt {a : Nat} {b : Nat} : ¬a < b → b ≤ a

theorem Nat.le_or_le (a : Nat) (b : Nat) : a ≤ b ∨ b ≤ a

theorem Nat.lt_or_eq_of_le {n : Nat} {m : Nat} (h : n ≤ m) : n < m ∨ n = m

theorem Nat.le_iff_lt_or_eq {n : Nat} {m : Nat} : n ≤ m ↔ n < m ∨ n = m

theorem Nat.le_antisymm_iff {n : Nat} {m : Nat} : n = m ↔ n ≤ m ∧ m ≤ n

zero/one

theorem Nat.pos_iff_ne_zero {n : Nat} : 0 < n ↔ n ≠ 0

theorem Nat.le_zero {i : Nat} : i ≤ 0 ↔ i = 0

theorem Nat.one_pos : 0 < 1

theorem Nat.add_one_ne_zero (n : Nat) : n + 1 ≠ 0

theorem Nat.eq_zero_of_nonpos (n : Nat) : ¬0 < n → n = 0

succ/pred

theorem Nat.succ_le {n : Nat} {m : Nat} : Nat.succ n ≤ m ↔ n < m

theorem Nat.lt_succ {m : Nat} {n : Nat} : m < Nat.succ n ↔ m ≤ n

theorem Nat.lt_succ_of_lt {a : Nat} {b : Nat} (h : a < b) : a < Nat.succ b

theorem Nat.succ_ne_self (n : Nat) : Nat.succ n ≠ n

theorem Nat.succ_pred_eq_of_pos {n : Nat} : 0 < n → Nat.succ (Nat.pred n) = n

theorem Nat.eq_zero_or_eq_succ_pred (n : Nat) : n = 0 ∨ n = Nat.succ (Nat.pred n)

theorem Nat.exists_eq_succ_of_ne_zero {n : Nat} (H : n ≠ 0) : ∃ k, n = Nat.succ k

theorem Nat.succ_eq_one_add (n : Nat) : Nat.succ n = 1 + n

theorem Nat.succ_inj' {n : Nat} {m : Nat} : Nat.succ n = Nat.succ m ↔ n = m

theorem Nat.pred_inj {a : Nat} {b : Nat} : 0 < a → 0 < b → Nat.pred a = Nat.pred b → a = b

theorem Nat.pred_lt_pred {n : Nat} {m : Nat} : n ≠ 0 → n < m → Nat.pred n < Nat.pred m

theorem Nat.succ_le_succ_iff {a : Nat} {b : Nat} : Nat.succ a ≤ Nat.succ b ↔ a ≤ b

theorem Nat.succ_lt_succ_iff {a : Nat} {b : Nat} : Nat.succ a < Nat.succ b ↔ a < b

theorem Nat.le_succ_of_pred_le {n : Nat} {m : Nat} : Nat.pred n ≤ m → n ≤ Nat.succ m

theorem Nat.le_pred_of_lt {m : Nat} {n : Nat} (h : m < n) : m ≤ n - 1

add

theorem Nat.eq_zero_of_add_eq_zero_right {n : Nat} {m : Nat} : n + m = 0 → n = 0

theorem Nat.eq_zero_of_add_eq_zero_left {n : Nat} {m : Nat} (h : n + m = 0) : m = 0

theorem Nat.succ_add_eq_succ_add (n : Nat) (m : Nat) : Nat.succ n + m = n + Nat.succ m

theorem Nat.one_add (n : Nat) : 1 + n = Nat.succ n

theorem Nat.eq_zero_of_add_eq_zero {n : Nat} {m : Nat} (H : n + m = 0) : n = 0 ∧ m = 0

theorem Nat.add_left_cancel_iff {n : Nat} {m : Nat} {k : Nat} : n + m = n + k ↔ m = k

theorem Nat.add_right_cancel_iff {n : Nat} {m : Nat} {k : Nat} : n + m = k + m ↔ n = k

theorem Nat.add_le_add_iff_left (k : Nat) (n : Nat) (m : Nat) : k + n ≤ k + m ↔ n ≤ m

theorem Nat.add_le_add_iff_right (k : Nat) (n : Nat) (m : Nat) : n + k ≤ m + k ↔ n ≤ m

theorem Nat.lt_of_add_lt_add_left {k : Nat} {n : Nat} {m : Nat} (h : k + n < k + m) : n < m

theorem Nat.lt_of_add_lt_add_right {a : Nat} {b : Nat} {c : Nat} (h : a + b < c + b) : a < c

theorem Nat.add_lt_add_iff_left (k : Nat) (n : Nat) (m : Nat) : k + n < k + m ↔ n < m

theorem Nat.add_lt_add_iff_right (k : Nat) (n : Nat) (m : Nat) : n + k < m + k ↔ n < m

theorem Nat.lt_add_right (a : Nat) (b : Nat) (c : Nat) (h : a < b) : a < b + c

theorem Nat.lt_add_of_pos_right {n : Nat} {k : Nat} (h : 0 < k) : n < n + k

theorem Nat.lt_add_of_pos_left {n : Nat} {k : Nat} (h : 0 < k) : n < k + n

theorem Nat.pos_of_lt_add_right {n : Nat} {k : Nat} (h : n < n + k) : 0 < k

theorem Nat.pos_of_lt_add_left {n : Nat} {k : Nat} (h : n < k + n) : 0 < k

theorem Nat.lt_add_right_iff_pos {n : Nat} {k : Nat} : n < n + k ↔ 0 < k

theorem Nat.lt_add_left_iff_pos {n : Nat} {k : Nat} : n < k + n ↔ 0 < k

theorem Nat.add_pos_left {m : Nat} (h : 0 < m) (n : Nat) : 0 < m + n

theorem Nat.add_pos_right {n : Nat} (m : Nat) (h : 0 < n) : 0 < m + n

theorem Nat.add_self_ne_one (n : Nat) : n + n ≠ 1

sub

theorem Nat.sub_lt_succ (a : Nat) (b : Nat) : a - b < Nat.succ a

theorem Nat.le_of_le_of_sub_le_sub_right {n : Nat} {m : Nat} {k : Nat} : k ≤ m → n - k ≤ m - k → n ≤ m

theorem Nat.sub_le_sub_iff_right {n : Nat} {m : Nat} {k : Nat} (h : k ≤ m) : n - k ≤ m - k ↔ n ≤ m

theorem Nat.add_le_to_le_sub (x : Nat) {y : Nat} {k : Nat} (h : k ≤ y) : x + k ≤ y ↔ x ≤ y - k

theorem Nat.sub_lt_of_pos_le {a : Nat} {b : Nat} (h₀ : 0 < a) (h₁ : a ≤ b) : b - a < b

theorem Nat.sub_one (n : Nat) : n - 1 = Nat.pred n

theorem Nat.succ_sub_one (n : Nat) : Nat.succ n - 1 = n

theorem Nat.le_of_sub_eq_zero {n : Nat} {m : Nat} : n - m = 0 → n ≤ m

theorem Nat.sub_eq_zero_iff_le {n : Nat} {m : Nat} : n - m = 0 ↔ n ≤ m

theorem Nat.sub_eq_iff_eq_add {a : Nat} {b : Nat} {c : Nat} (ab : b ≤ a) : a - b = c ↔ a = c + b

theorem Nat.lt_of_sub_eq_succ {m : Nat} {n : Nat} {l : Nat} (H : m - n = Nat.succ l) : n < m

theorem Nat.sub_le_sub_left {n : Nat} {m : Nat} (k : Nat) (h : n ≤ m) : k - m ≤ k - n

theorem Nat.succ_sub_sub_succ (n : Nat) (m : Nat) (k : Nat) : Nat.succ n - m - Nat.succ k = n - m - k

theorem Nat.sub_right_comm (m : Nat) (n : Nat) (k : Nat) : m - n - k = m - k - n

theorem Nat.sub_pos_of_lt {m : Nat} {n : Nat} (h : m < n) : 0 < n - m

theorem Nat.sub_sub_self {n : Nat} {m : Nat} (h : m ≤ n) : n - (n - m) = m

theorem Nat.sub_add_comm {n : Nat} {m : Nat} {k : Nat} (h : k ≤ n) : n + m - k = n - k + m

theorem Nat.sub_one_sub_lt {i : Nat} {n : Nat} (h : i < n) : n - 1 - i < n

theorem Nat.sub_lt_self {a : Nat} {b : Nat} (h₀ : 0 < a) (h₁ : a ≤ b) : b - a < b

theorem Nat.add_sub_cancel' {n : Nat} {m : Nat} (h : m ≤ n) : m + (n - m) = n

theorem Nat.add_le_of_le_sub_left {n : Nat} {k : Nat} {m : Nat} (H : m ≤ k) (h : n ≤ k - m) : m + n ≤ k

theorem Nat.le_sub_iff_add_le {x : Nat} {y : Nat} {k : Nat} (h : k ≤ y) : x ≤ y - k ↔ x + k ≤ y

theorem Nat.sub_le_iff_le_add {a : Nat} {b : Nat} {c : Nat} : a - b ≤ c ↔ a ≤ c + b

theorem Nat.sub_le_iff_le_add' {a : Nat} {b : Nat} {c : Nat} : a - b ≤ c ↔ a ≤ b + c

theorem Nat.sub_le_sub_iff_left {n : Nat} {m : Nat} {k : Nat} (hn : n ≤ k) : k - m ≤ k - n ↔ n ≤ m

theorem Nat.sub_add_lt_sub {n : Nat} {m : Nat} {k : Nat} (h₁ : m + k ≤ n) (h₂ : 0 < k) : n - (m + k) < n - m

min/max

theorem Nat.le_min {a : Nat} {b : Nat} {c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c

theorem Nat.lt_min {a : Nat} {b : Nat} {c : Nat} : a < min b c ↔ a < b ∧ a < c

theorem Nat.min_eq_left {a : Nat} {b : Nat} (h : a ≤ b) : min a b = a

theorem Nat.min_eq_right {a : Nat} {b : Nat} (h : b ≤ a) : min a b = b

theorem Nat.zero_min (a : Nat) : min 0 a = 0

theorem Nat.min_zero (a : Nat) : min a 0 = 0

theorem Nat.max_le {a : Nat} {b : Nat} {c : Nat} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c

theorem Nat.max_eq_right {a : Nat} {b : Nat} (h : a ≤ b) : max a b = b

theorem Nat.max_eq_left {a : Nat} {b : Nat} (h : b ≤ a) : max a b = a

theorem Nat.min_succ_succ (x : Nat) (y : Nat) : min (Nat.succ x) (Nat.succ y) = Nat.succ (min x y)

theorem Nat.sub_eq_sub_min (n : Nat) (m : Nat) : n - m = n - min n m

@[simp]

theorem Nat.sub_add_min_cancel (n : Nat) (m : Nat) : n - m + min n m = n

theorem Nat.sub_add_eq_max {a : Nat} {b : Nat} : a - b + b = max a b

mul

theorem Nat.mul_right_comm (n : Nat) (m : Nat) (k : Nat) : n * m * k = n * k * m

theorem Nat.mul_mul_mul_comm (a : Nat) (b : Nat) (c : Nat) (d : Nat) : a * b * (c * d) = a * c * (b * d)

theorem Nat.mul_two (n : Nat) : n * 2 = n + n

theorem Nat.two_mul (n : Nat) : 2 * n = n + n

theorem Nat.mul_eq_zero {n : Nat} {m : Nat} : n * m = 0 ↔ n = 0 ∨ m = 0

theorem Nat.mul_ne_zero_iff {n : Nat} {m : Nat} : n * m ≠ 0 ↔ n ≠ 0 ∧ m ≠ 0

theorem Nat.mul_ne_zero {n : Nat} {m : Nat} (n0 : n ≠ 0) (m0 : m ≠ 0) : n * m ≠ 0

theorem Nat.mul_le_mul_of_nonneg_left {a : Nat} {b : Nat} {c : Nat} (h₁ : a ≤ b) : c * a ≤ c * b

theorem Nat.mul_le_mul_of_nonneg_right {a : Nat} {b : Nat} {c : Nat} (h₁ : a ≤ b) : a * c ≤ b * c

theorem Nat.mul_lt_mul {a : Nat} {c : Nat} {b : Nat} {d : Nat} (hac : a < c) (hbd : b ≤ d) (pos_b : 0 < b) : a * b < c * d

theorem Nat.mul_lt_mul' {a : Nat} {c : Nat} {b : Nat} {d : Nat} (h1 : a ≤ c) (h2 : b < d) (h3 : 0 < c) : a * b < c * d

theorem Nat.succ_mul_succ_eq (a : Nat) (b : Nat) : Nat.succ a * Nat.succ b = a * b + a + b + 1

theorem Nat.mul_self_sub_mul_self_eq (a : Nat) (b : Nat) : a * a - b * b = (a + b) * (a - b)

div/mod

theorem Nat.mod_add_div (m : Nat) (k : Nat) : m % k + k * (m / k) = m

@[simp]

theorem Nat.div_one (n : Nat) : n / 1 = n

@[simp]

theorem Nat.div_zero (n : Nat) : n / 0 = 0

@[simp]

theorem Nat.zero_div (b : Nat) : 0 / b = 0

theorem Nat.le_div_iff_mul_le {k : Nat} {x : Nat} {y : Nat} (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y

theorem Nat.div_le_of_le_mul {m : Nat} {n : Nat} {k : Nat} : m ≤ k * n → m / k ≤ n

theorem Nat.div_eq_sub_div {b : Nat} {a : Nat} (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1

theorem Nat.div_eq_of_lt {a : Nat} {b : Nat} (h₀ : a < b) : a / b = 0

theorem Nat.div_lt_iff_lt_mul {k : Nat} {x : Nat} {y : Nat} (Hk : 0 < k) : x / k < y ↔ x < y * k

theorem Nat.sub_mul_div (x : Nat) (n : Nat) (p : Nat) (h₁ : n * p ≤ x) : (x - n * p) / n = x / n - p

theorem Nat.div_mul_le_self (m : Nat) (n : Nat) : m / n * n ≤ m

@[simp]

theorem Nat.add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = Nat.succ (x / z)

@[simp]

theorem Nat.add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = Nat.succ (x / z)

@[simp]

theorem Nat.mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n

@[simp]

theorem Nat.mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m

theorem Nat.div_self {n : Nat} (H : 0 < n) : n / n = 1

theorem Nat.add_mul_div_left (x : Nat) (z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z

theorem Nat.add_mul_div_right (x : Nat) (y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y

theorem Nat.mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m

theorem Nat.mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m

theorem Nat.div_eq_of_eq_mul_left {n : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = k * n) : m / n = k

theorem Nat.div_eq_of_eq_mul_right {n : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = n * k) : m / n = k

theorem Nat.div_eq_of_lt_le {k : Nat} {n : Nat} {m : Nat} (lo : k * n ≤ m) (hi : m < Nat.succ k * n) : m / n = k

theorem Nat.mul_sub_div (x : Nat) (n : Nat) (p : Nat) (h₁ : x < n * p) : (n * p - Nat.succ x) / n = p - Nat.succ (x / n)

theorem Nat.div_div_eq_div_mul (m : Nat) (n : Nat) (k : Nat) : m / n / k = m / (n * k)

theorem Nat.mul_div_mul_left {m : Nat} (n : Nat) (k : Nat) (H : 0 < m) : m * n / (m * k) = n / k

theorem Nat.mul_div_mul_right {m : Nat} (n : Nat) (k : Nat) (H : 0 < m) : n * m / (k * m) = n / k

theorem Nat.mul_div_le (m : Nat) (n : Nat) : n * (m / n) ≤ m

theorem Nat.mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1

theorem Nat.le_of_mod_lt {a : Nat} {b : Nat} (h : a % b < a) : b ≤ a

@[simp]

theorem Nat.add_mod_right (x : Nat) (z : Nat) : (x + z) % z = x % z

@[simp]

theorem Nat.add_mod_left (x : Nat) (z : Nat) : (x + z) % x = z % x

@[simp]

theorem Nat.add_mul_mod_self_left (x : Nat) (y : Nat) (z : Nat) : (x + y * z) % y = x % y

@[simp]

theorem Nat.add_mul_mod_self_right (x : Nat) (y : Nat) (z : Nat) : (x + y * z) % z = x % z

@[simp]

theorem Nat.mul_mod_right (m : Nat) (n : Nat) : m * n % m = 0

@[simp]

theorem Nat.mul_mod_left (m : Nat) (n : Nat) : m * n % n = 0

theorem Nat.mul_mod_mul_left (z : Nat) (x : Nat) (y : Nat) : z * x % (z * y) = z * (x % y)

theorem Nat.mul_mod_mul_right (z : Nat) (x : Nat) (y : Nat) : x * z % (y * z) = x % y * z

theorem Nat.sub_mul_mod {x : Nat} {k : Nat} {n : Nat} (h₁ : n * k ≤ x) : (x - n * k) % n = x % n

@[simp]

theorem Nat.mod_mod (a : Nat) (n : Nat) : a % n % n = a % n

theorem Nat.mul_mod (a : Nat) (b : Nat) (n : Nat) : a * b % n = a % n * (b % n) % n

@[simp]

theorem Nat.mod_add_mod (m : Nat) (n : Nat) (k : Nat) : (m % n + k) % n = (m + k) % n

@[simp]

theorem Nat.add_mod_mod (m : Nat) (n : Nat) (k : Nat) : (m + n % k) % k = (m + n) % k

theorem Nat.add_mod (a : Nat) (b : Nat) (n : Nat) : (a + b) % n = (a % n + b % n) % n

pow

theorem Nat.pow_succ' {m : Nat} {n : Nat} : m ^ Nat.succ n = m * m ^ n

@[simp]

theorem Nat.pow_eq {m : Nat} {n : Nat} : Nat.pow m n = m ^ n

@[simp]

theorem Nat.shiftLeft_eq (a : Nat) (b : Nat) : a <<< b = a * 2 ^ b

theorem Nat.one_shiftLeft (n : Nat) : 1 <<< n = 2 ^ n

theorem Nat.zero_pow {n : Nat} (H : 0 < n) : 0 ^ n = 0

@[simp]

theorem Nat.one_pow (n : Nat) : 1 ^ n = 1

@[simp]

theorem Nat.pow_one (a : Nat) : a ^ 1 = a

theorem Nat.pow_two (a : Nat) : a ^ 2 = a * a

theorem Nat.pow_add (a : Nat) (m : Nat) (n : Nat) : a ^ (m + n) = a ^ m * a ^ n

theorem Nat.pow_add' (a : Nat) (m : Nat) (n : Nat) : a ^ (m + n) = a ^ n * a ^ m

theorem Nat.pow_mul (a : Nat) (m : Nat) (n : Nat) : a ^ (m * n) = (a ^ m) ^ n

theorem Nat.pow_mul' (a : Nat) (m : Nat) (n : Nat) : a ^ (m * n) = (a ^ n) ^ m

theorem Nat.pow_right_comm (a : Nat) (m : Nat) (n : Nat) : (a ^ m) ^ n = (a ^ n) ^ m

theorem Nat.mul_pow (a : Nat) (b : Nat) (n : Nat) : (a * b) ^ n = a ^ n * b ^ n

log2

theorem Nat.le_log2 {n : Nat} {k : Nat} (h : n ≠ 0) : k ≤ Nat.log2 n ↔ 2 ^ k ≤ n

theorem Nat.log2_lt {n : Nat} {k : Nat} (h : n ≠ 0) : Nat.log2 n < k ↔ n < 2 ^ k

theorem Nat.log2_self_le {n : Nat} (h : n ≠ 0) : 2 ^ Nat.log2 n ≤ n

theorem Nat.lt_log2_self {n : Nat} (h : n ≠ 0) : n < 2 ^ (Nat.log2 n + 1)

dvd

theorem Nat.dvd_refl (a : Nat) : a ∣ a

theorem Nat.dvd_zero (a : Nat) : a ∣ 0

theorem Nat.dvd_mul_left (a : Nat) (b : Nat) : a ∣ b * a

theorem Nat.dvd_mul_right (a : Nat) (b : Nat) : a ∣ a * b

theorem Nat.dvd_trans {a : Nat} {b : Nat} {c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c

theorem Nat.eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0

theorem Nat.dvd_add {a : Nat} {b : Nat} {c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c

theorem Nat.dvd_add_iff_right {k : Nat} {m : Nat} {n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n

theorem Nat.dvd_add_iff_left {k : Nat} {m : Nat} {n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n

theorem Nat.dvd_sub {k : Nat} {m : Nat} {n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n

theorem Nat.mul_dvd_mul {a : Nat} {b : Nat} {c : Nat} {d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d

theorem Nat.mul_dvd_mul_left {b : Nat} {c : Nat} (a : Nat) (h : b ∣ c) : a * b ∣ a * c

theorem Nat.mul_dvd_mul_right {a : Nat} {b : Nat} (h : a ∣ b) (c : Nat) : a * c ∣ b * c

theorem Nat.dvd_mod_iff {k : Nat} {m : Nat} {n : Nat} (h : k ∣ n) : k ∣ m % n ↔ k ∣ m

theorem Nat.le_of_dvd {m : Nat} {n : Nat} (h : 0 < n) : m ∣ n → m ≤ n

theorem Nat.dvd_antisymm {m : Nat} {n : Nat} : m ∣ n → n ∣ m → m = n

theorem Nat.pos_of_dvd_of_pos {m : Nat} {n : Nat} (H1 : m ∣ n) (H2 : 0 < n) : 0 < m

theorem Nat.eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1

theorem Nat.dvd_of_mod_eq_zero {m : Nat} {n : Nat} (H : n % m = 0) : m ∣ n

theorem Nat.mod_eq_zero_of_dvd {m : Nat} {n : Nat} (H : m ∣ n) : n % m = 0

theorem Nat.dvd_iff_mod_eq_zero (m : Nat) (n : Nat) : m ∣ n ↔ n % m = 0

instance Nat.decidable_dvd : DecidableRel fun x x_1 => x ∣ x_1

Equations

• Nat.decidable_dvd x x = decidable_of_decidable_of_iff (_ : x % x = 0 ↔ x ∣ x)

theorem Nat.mul_div_cancel' {n : Nat} {m : Nat} (H : n ∣ m) : n * (m / n) = m

theorem Nat.div_mul_cancel {n : Nat} {m : Nat} (H : n ∣ m) : m / n * n = m

theorem Nat.mul_div_assoc {k : Nat} {n : Nat} (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k)

theorem Nat.dvd_of_mul_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n

theorem Nat.dvd_of_mul_dvd_mul_right {k : Nat} {m : Nat} {n : Nat} (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n

sum

@[simp]

theorem Nat.sum_nil : Nat.sum [] = 0

@[simp]

theorem Nat.sum_cons {a : Nat} {l : List Nat} : Nat.sum (a :: l) = a + Nat.sum l

@[simp]

theorem Nat.sum_append {l₁ : List Nat} {l₂ : List Nat} : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂