mathlib documentation

theorem nat.add_comm (n m : ℕ) :

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

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

theorem nat.add_left_cancel {n m k : ℕ} (a : n + m = n + k) :

theorem nat.add_right_cancel {n m k : ℕ} (h : n + m = k + m) :

theorem nat.succ_ne_zero (n : ℕ) :

theorem nat.succ_ne_self (n : ℕ) :

theorem nat.one_ne_zero  :

theorem nat.zero_ne_one  :

theorem nat.eq_zero_of_add_eq_zero_right {n m : ℕ} (a : n + m = 0) :

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

theorem nat.pred_zero  :

theorem nat.pred_succ (n : ℕ) :

theorem nat.mul_zero (n : ℕ) :

theorem nat.mul_succ (n m : ℕ) :

theorem nat.zero_mul (n : ℕ) :

theorem nat.succ_mul (n m : ℕ) :

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

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

theorem nat.mul_comm (n m : ℕ) :

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

theorem nat.mul_one (n : ℕ) :

theorem nat.one_mul (n : ℕ) :

theorem nat.le_of_eq {n m : ℕ} (p : n = m) :

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

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

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

theorem nat.eq_zero_or_pos (n : ℕ) :

theorem nat.pos_of_ne_zero {n : ℕ} (a : n ≠ 0) :

theorem nat.lt_trans {n m k : ℕ} (h₁ : n < m) (a : m < k) :

theorem nat.lt_of_le_of_lt {n m k : ℕ} (h₁ : n ≤ m) (a : m < k) :

theorem nat.lt_succ_self (n : ℕ) :

theorem nat.le_antisymm {n m : ℕ} (h₁ : n ≤ m) (a : m ≤ n) :

theorem nat.lt_or_ge (a b : ℕ) :

theorem nat.le_total {m n : ℕ} :

theorem nat.lt_of_le_and_ne {m n : ℕ} (h1 : m ≤ n) (a : m ≠ n) :

theorem nat.lt_iff_le_not_le {m n : ℕ} :

theorem nat.eq_zero_of_le_zero {n : ℕ} (h : n ≤ 0) :

theorem nat.succ_lt_succ {a b : ℕ} (a_1 : a < b) :

theorem nat.lt_of_succ_lt {a b : ℕ} (a_1 : a.succ < b) :

theorem nat.lt_of_succ_lt_succ {a b : ℕ} (a_1 : a.succ < b.succ) :

theorem nat.pred_lt_pred {n m : ℕ} (a : n ≠ 0) (a_1 : n < m) :

theorem nat.lt_of_succ_le {a b : ℕ} (h : a.succ ≤ b) :

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

theorem nat.le_add_right (n k : ℕ) :

theorem nat.le_add_left (n m : ℕ) :

theorem nat.le.dest {n m : ℕ} (a : n ≤ m) :

theorem nat.le.intro {n m k : ℕ} (h : n + k = m) :

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

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

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

theorem nat.le_of_add_le_add_right {k n m : ℕ} (a : n + k ≤ m + k) :

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

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

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

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

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

theorem nat.lt_add_of_pos_right {n k : ℕ} (h : k > 0) :

theorem nat.lt_add_of_pos_left {n k : ℕ} (h : k > 0) :

theorem nat.add_lt_add {a b c d : ℕ} (h₁ : a < b) (h₂ : c < d) :

theorem nat.add_le_add {a b c d : ℕ} (h₁ : a ≤ b) (h₂ : c ≤ d) :

theorem nat.zero_lt_one  :

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

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

theorem nat.mul_lt_mul_of_pos_left {n m k : ℕ} (h : n < m) (hk : k > 0) :

theorem nat.mul_lt_mul_of_pos_right {n m k : ℕ} (h : n < m) (hk : k > 0) :

theorem nat.le_of_mul_le_mul_left {a b c : ℕ} (h : c * a ≤ c * b) (hc : c > 0) :

theorem nat.le_of_lt_succ {m n : ℕ} (a : m < n.succ) :

theorem nat.eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) :

theorem nat.zero_sub (a : ℕ) :

theorem nat.sub_lt_succ (a b : ℕ) :

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

theorem nat.bit1_eq_succ_bit0 (n : ℕ) :

theorem nat.bit1_succ_eq (n : ℕ) :

theorem nat.bit1_ne_one {n : ℕ} (a : n ≠ 0) :

theorem nat.bit0_ne_one (n : ℕ) :

theorem nat.add_self_ne_one (n : ℕ) :

theorem nat.bit1_ne_bit0 (n m : ℕ) :

theorem nat.bit0_ne_bit1 (n m : ℕ) :

theorem nat.bit0_inj {n m : ℕ} (a : bit0 n = bit0 m) :

theorem nat.bit1_inj {n m : ℕ} (a : bit1 n = bit1 m) :

theorem nat.bit0_ne {n m : ℕ} (a : n ≠ m) :

theorem nat.bit1_ne {n m : ℕ} (a : n ≠ m) :

theorem nat.zero_ne_bit0 {n : ℕ} (a : n ≠ 0) :

theorem nat.zero_ne_bit1 (n : ℕ) :

theorem nat.one_ne_bit0 (n : ℕ) :

theorem nat.one_ne_bit1 {n : ℕ} (a : n ≠ 0) :

theorem nat.one_lt_bit1 {n : ℕ} (a : n ≠ 0) :

theorem nat.one_lt_bit0 {n : ℕ} (a : n ≠ 0) :

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

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

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

theorem nat.bit1_lt_bit0 {n m : ℕ} (a : n < m) :

theorem nat.one_le_bit1 (n : ℕ) :

theorem nat.one_le_bit0 (n : ℕ) (a : n ≠ 0) :

theorem nat.sub_zero (n : ℕ) :

theorem nat.sub_succ (n m : ℕ) :

theorem nat.succ_sub_succ (n m : ℕ) :

theorem nat.sub_self (n : ℕ) :

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

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

theorem nat.add_sub_cancel (n m : ℕ) :

theorem nat.add_sub_cancel_left (n m : ℕ) :

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

theorem nat.le_of_le_of_sub_le_sub_right {n m k : ℕ} (h₀ : k ≤ m) (h₁ : n - k ≤ m - k) :

theorem nat.sub_le_sub_right_iff (n m k : ℕ) (h : k ≤ m) :

theorem nat.sub_self_add (n m : ℕ) :

theorem nat.add_le_to_le_sub (x : ℕ) {y k : ℕ} (h : k ≤ y) :

theorem nat.sub_lt_of_pos_le (a b : ℕ) (h₀ : 0 < a) (h₁ : a ≤ b) :

theorem nat.sub_one (n : ℕ) :

theorem nat.succ_sub_one (n : ℕ) :

theorem nat.succ_pred_eq_of_pos {n : ℕ} (a : n > 0) :

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

theorem nat.le_of_sub_eq_zero {n m : ℕ} (a : n - m = 0) :

theorem nat.sub_eq_zero_iff_le {n m : ℕ} :

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

theorem nat.sub_add_cancel {n m : ℕ} (h : n ≥ m) :

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

theorem nat.sub_eq_iff_eq_add {a b c : ℕ} (ab : b ≤ a) :

theorem nat.lt_of_sub_eq_succ {m n l : ℕ} (H : m - n = l.succ) :

theorem nat.zero_min (a : ℕ) :

theorem nat.min_zero (a : ℕ) :

theorem nat.min_succ_succ (x y : ℕ) :

theorem nat.sub_eq_sub_min (n m : ℕ) :

theorem nat.sub_add_min_cancel (n m : ℕ) :

theorem nat.strong_induction_on {p : ℕ → Prop} (n : ℕ) (h : ∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n) :

theorem nat.case_strong_induction_on {p : ℕ → Prop} (a : ℕ) (hz : p 0) (hi : ∀ (n : ℕ), (∀ (m : ℕ), m ≤ n → p m) → p n.succ) :

theorem nat.mod_def (x y : ℕ) :

theorem nat.mod_zero (a : ℕ) :

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

theorem nat.zero_mod (b : ℕ) :

theorem nat.mod_eq_sub_mod {a b : ℕ} (h : a ≥ b) :

theorem nat.mod_lt (x : ℕ) {y : ℕ} (h : y > 0) :

theorem nat.mod_self (n : ℕ) :

theorem nat.mod_one (n : ℕ) :

theorem nat.mod_two_eq_zero_or_one (n : ℕ) :

theorem nat.div_def (x y : ℕ) :

theorem nat.mod_add_div (m k : ℕ) :

theorem nat.div_one (n : ℕ) :

theorem nat.div_zero (n : ℕ) :

theorem nat.zero_div (b : ℕ) :

theorem nat.div_le_of_le_mul {m n k : ℕ} (a : m ≤ k * n) :

theorem nat.div_le_self (m n : ℕ) :

theorem nat.div_eq_sub_div {a b : ℕ} (h₁ : b > 0) (h₂ : a ≥ b) :

theorem nat.div_eq_of_lt {a b : ℕ} (h₀ : a < b) :

theorem nat.le_div_iff_mul_le (x y : ℕ) {k : ℕ} (Hk : k > 0) :

theorem nat.div_lt_iff_lt_mul (x y : ℕ) {k : ℕ} (Hk : k > 0) :

theorem nat.add_one_ne_zero (n : ℕ) :

theorem nat.eq_zero_or_eq_succ_pred (n : ℕ) :

theorem nat.exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) :

theorem nat.discriminate {B : Sort u} {n : ℕ} (H1 : n = 0 → B) (H2 : Π (m : ℕ), n = m.succ → B) :

theorem nat.one_succ_zero  :

theorem nat.two_step_induction {P : ℕ → Sort u} (H1 : P 0) (H2 : P 1) (H3 : Π (n : ℕ), P n → P n.succ → P n.succ.succ) (a : ℕ) :

theorem nat.sub_induction {P : ℕ → ℕ → Sort u} (H1 : Π (m : ℕ), P 0 m) (H2 : Π (n : ℕ), P n.succ 0) (H3 : Π (n m : ℕ), P n m → P n.succ m.succ) (n m : ℕ) :

theorem nat.succ_add_eq_succ_add (n m : ℕ) :

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

theorem nat.eq_zero_of_add_eq_zero {n m : ℕ} (H : n + m = 0) :

theorem nat.eq_zero_of_mul_eq_zero {n m : ℕ} (a : n * m = 0) :

theorem nat.le_succ_of_pred_le {n m : ℕ} (a : n.pred ≤ m) :

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

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

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

theorem nat.lt_trichotomy (a b : ℕ) :

theorem nat.eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬a < b) :

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

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

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

theorem nat.sub.right_comm (m n k : ℕ) :

theorem nat.mul_pred_left (n m : ℕ) :

theorem nat.mul_pred_right (n m : ℕ) :

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

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

theorem nat.mul_self_sub_mul_self_eq (a b : ℕ) :

theorem nat.succ_mul_succ_eq (a b : ℕ) :

theorem nat.succ_sub {m n : ℕ} (h : m ≥ n) :

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

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

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

theorem nat.sub_one_sub_lt {n i : ℕ} (h : i < n) :

theorem nat.pred_inj {a b : ℕ} (a_1 : a > 0) (a_2 : b > 0) (a_3 : a.pred = b.pred) :

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

theorem nat.find_min {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) {m : ℕ} (a : m < nat.find H) :

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

theorem nat.mod_le (x y : ℕ) :

theorem nat.add_mod_right (x z : ℕ) :

theorem nat.add_mod_left (x z : ℕ) :

theorem nat.add_mul_mod_self_left (x y z : ℕ) :

theorem nat.add_mul_mod_self_right (x y z : ℕ) :

theorem nat.mul_mod_right (m n : ℕ) :

theorem nat.mul_mod_left (m n : ℕ) :

theorem nat.mul_mod_mul_left (z x y : ℕ) :

theorem nat.mul_mod_mul_right (z x y : ℕ) :

theorem nat.cond_to_bool_mod_two (x : ℕ) [d : decidable (x % 2 = 1)] :

theorem nat.sub_mul_mod (x k n : ℕ) (h₁ : n * k ≤ x) :

theorem nat.sub_mul_div (x n p : ℕ) (h₁ : n * p ≤ x) :

theorem nat.div_mul_le_self (m n : ℕ) :

theorem nat.add_div_right (x : ℕ) {z : ℕ} (H : z > 0) :

theorem nat.add_div_left (x : ℕ) {z : ℕ} (H : z > 0) :

theorem nat.mul_div_right (n : ℕ) {m : ℕ} (H : m > 0) :

theorem nat.mul_div_left (m : ℕ) {n : ℕ} (H : n > 0) :

theorem nat.div_self {n : ℕ} (H : n > 0) :

theorem nat.add_mul_div_left (x z : ℕ) {y : ℕ} (H : y > 0) :

theorem nat.add_mul_div_right (x y : ℕ) {z : ℕ} (H : z > 0) :

theorem nat.mul_div_cancel (m : ℕ) {n : ℕ} (H : n > 0) :

theorem nat.mul_div_cancel_left (m : ℕ) {n : ℕ} (H : n > 0) :

theorem nat.div_eq_of_eq_mul_left {m n k : ℕ} (H1 : n > 0) (H2 : m = k * n) :

theorem nat.div_eq_of_eq_mul_right {m n k : ℕ} (H1 : n > 0) (H2 : m = n * k) :

theorem nat.div_eq_of_lt_le {m n k : ℕ} (lo : k * n ≤ m) (hi : m < (k.succ) * n) :

theorem nat.mul_sub_div (x n p : ℕ) (h₁ : x < n * p) :

theorem nat.mul_pos {a b : ℕ} (ha : a > 0) (hb : b > 0) :

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

theorem nat.mul_div_mul {m : ℕ} (n k : ℕ) (H : m > 0) :

theorem nat.dvd_mul_right (a b : ℕ) :

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

theorem nat.eq_zero_of_zero_dvd {a : ℕ} (h : 0 ∣ a) :

theorem nat.dvd_add {a b c : ℕ} (h₁ : a ∣ b) (h₂ : a ∣ c) :

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

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

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

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

theorem nat.le_of_dvd {m n : ℕ} (h : n > 0) (a : m ∣ n) :

theorem nat.dvd_antisymm {m n : ℕ} (a : m ∣ n) (a_1 : n ∣ m) :

theorem nat.pos_of_dvd_of_pos {m n : ℕ} (H1 : m ∣ n) (H2 : n > 0) :

theorem nat.eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) :

theorem nat.dvd_of_mod_eq_zero {m n : ℕ} (H : n % m = 0) :

theorem nat.mod_eq_zero_of_dvd {m n : ℕ} (H : m ∣ n) :

theorem nat.dvd_iff_mod_eq_zero (m n : ℕ) :

theorem nat.mul_div_cancel' {m n : ℕ} (H : n ∣ m) :

theorem nat.div_mul_cancel {m n : ℕ} (H : n ∣ m) :

theorem nat.mul_div_assoc (m : ℕ) {n k : ℕ} (H : k ∣ n) :

theorem nat.dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : k > 0) (H : k * m ∣ k * n) :

theorem nat.dvd_of_mul_dvd_mul_right {m n k : ℕ} (kpos : k > 0) (H : m * k ∣ n * k) :

theorem nat.mul_le_mul_of_nonneg_left {a b c : ℕ} (h₁ : a ≤ b) :

theorem nat.mul_le_mul_of_nonneg_right {a b c : ℕ} (h₁ : a ≤ b) :

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

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

theorem nat.mul_le_mul {a b c d : ℕ} (hac : a ≤ c) (hbd : b ≤ d) :

theorem nat.div_lt_self {n m : ℕ} (a : n > 0) (a_1 : m > 1) :