mathlib documentation

theorem int.ne_neg_of_ne {a b : ℤ} (a_1 : a ≠ b) :

theorem int.neg_ne_zero_of_ne {a : ℤ} (a_1 : a ≠ 0) :

theorem int.zero_ne_neg_of_ne {a : ℤ} (h : 0 ≠ a) :

theorem int.neg_ne_of_pos {a b : ℤ} (a_1 : a > 0) (a_2 : b > 0) :

theorem int.ne_neg_of_pos {a b : ℤ} (a_1 : a > 0) (a_2 : b > 0) :

theorem int.one_pos  :

theorem int.bit0_pos {a : ℤ} (a_1 : a > 0) :

theorem int.bit1_pos {a : ℤ} (a_1 : a ≥ 0) :

theorem int.zero_nonneg  :

theorem int.one_nonneg  :

theorem int.bit0_nonneg {a : ℤ} (a_1 : a ≥ 0) :

theorem int.bit1_nonneg {a : ℤ} (a_1 : a ≥ 0) :

theorem int.nonneg_of_pos {a : ℤ} (a_1 : a > 0) :

theorem int.neg_succ_of_nat_lt_zero (n : ℕ) :

theorem int.of_nat_ge_zero (n : ℕ) :

theorem int.of_nat_nat_abs_eq_of_nonneg {a : ℤ} (a_1 : a ≥ 0) :

theorem int.ne_of_nat_abs_ne_nat_abs_of_nonneg {a b : ℤ} (ha : a ≥ 0) (hb : b ≥ 0) (h : a.nat_abs ≠ b.nat_abs) :

theorem int.ne_of_nat_ne_nonneg_case {a b : ℤ} {n m : ℕ} (ha : a ≥ 0) (hb : b ≥ 0) (e1 : a.nat_abs = n) (e2 : b.nat_abs = m) (h : n ≠ m) :

theorem int.nat_abs_of_nat_core (n : ℕ) :

theorem int.nat_abs_of_neg_succ_of_nat (n : ℕ) :

theorem int.nat_abs_add_nonneg {a b : ℤ} (a_1 : a ≥ 0) (a_2 : b ≥ 0) :

theorem int.nat_abs_add_neg {a b : ℤ} (a_1 : a < 0) (a_2 : b < 0) :

theorem int.nat_abs_bit0 (a : ℤ) :

theorem int.nat_abs_bit0_step {a : ℤ} {n : ℕ} (h : a.nat_abs = n) :

theorem int.nat_abs_bit1_nonneg {a : ℤ} (h : a ≥ 0) :

theorem int.nat_abs_bit1_nonneg_step {a : ℤ} {n : ℕ} (h₁ : a ≥ 0) (h₂ : a.nat_abs = n) :