[GOAL]
a : ℤ
h₁ : a ≠ 0
h₂ : -a = 0
⊢ False
[PROOFSTEP]
have : -a = -0 := by rwa [Int.neg_zero]
[GOAL]
a : ℤ
h₁ : a ≠ 0
h₂ : -a = 0
⊢ -a = -0
[PROOFSTEP]
rwa [Int.neg_zero]
[GOAL]
a : ℤ
h₁ : a ≠ 0
h₂ : -a = 0
this : -a = -0
⊢ False
[PROOFSTEP]
have : a = 0 := Int.neg_eq_neg this
[GOAL]
a : ℤ
h₁ : a ≠ 0
h₂ : -a = 0
this✝ : -a = -0
this : a = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
a b : ℤ
h₁ : 0 < a
h₂ : 0 < b
h : -a = b
⊢ False
[PROOFSTEP]
rw [← h] at h₂ 
[GOAL]
a b : ℤ
h₁ : 0 < a
h₂ : 0 < -a
h : -a = b
⊢ False
[PROOFSTEP]
exact absurd (le_of_lt h₁) (not_le_of_gt (Int.neg_of_neg_pos h₂))
[GOAL]
n : ℕ
⊢ 0 + ↑n = ofNat n
[PROOFSTEP]
rw [Int.zero_add, Int.coe_nat_eq]
[GOAL]
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : natAbs a ≠ natAbs b
h : a = b
⊢ False
[PROOFSTEP]
have : (natAbs a : ℤ) = natAbs b := by rwa [ofNat_natAbs_eq_of_nonneg _ ha, ofNat_natAbs_eq_of_nonneg _ hb]
[GOAL]
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : natAbs a ≠ natAbs b
h : a = b
⊢ ↑(natAbs a) = ↑(natAbs b)
[PROOFSTEP]
rwa [ofNat_natAbs_eq_of_nonneg _ ha, ofNat_natAbs_eq_of_nonneg _ hb]
[GOAL]
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : natAbs a ≠ natAbs b
h : a = b
this : ↑(natAbs a) = ↑(natAbs b)
⊢ False
[PROOFSTEP]
injection this
[GOAL]
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : natAbs a ≠ natAbs b
h : a = b
a_eq✝ : natAbs a = natAbs b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
a b : ℤ
n m : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
e1 : natAbs a = n
e2 : natAbs b = m
h : n ≠ m
⊢ natAbs a ≠ natAbs b
[PROOFSTEP]
rwa [e1, e2]
[GOAL]
n m : ℕ
x✝¹ : 0 ≤ ofNat n
x✝ : 0 ≤ ofNat m
⊢ natAbs (ofNat n + ofNat m) = natAbs (ofNat n) + natAbs (ofNat m)
[PROOFSTEP]
simp [natAbs_ofNat_core]
[GOAL]
n m : ℕ
x✝¹ : -[n+1] < 0
x✝ : -[m+1] < 0
⊢ natAbs (-[n+1] + -[m+1]) = natAbs -[n+1] + natAbs -[m+1]
[PROOFSTEP]
simp [natAbs_of_negSucc, Nat.succ_add, Nat.add_succ]
[GOAL]
a : ℤ
n : ℕ
h : natAbs a = n
⊢ natAbs (bit0 a) = bit0 n
[PROOFSTEP]
rw [← h]
[GOAL]
a : ℤ
n : ℕ
h : natAbs a = n
⊢ natAbs (bit0 a) = bit0 (natAbs a)
[PROOFSTEP]
apply Int.natAbs_bit0
[GOAL]
a : ℤ
h : 0 ≤ a
⊢ natAbs (bit0 a + 1) = bit0 (natAbs a) + natAbs 1
[PROOFSTEP]
rw [Int.natAbs_add_nonneg (Int.bit0_nonneg h) (le_of_lt Int.zero_lt_one), Int.natAbs_bit0]
[GOAL]
a : ℤ
n : ℕ
h₁ : 0 ≤ a
h₂ : natAbs a = n
⊢ natAbs (bit1 a) = bit1 n
[PROOFSTEP]
rw [← h₂]
[GOAL]
a : ℤ
n : ℕ
h₁ : 0 ≤ a
h₂ : natAbs a = n
⊢ natAbs (bit1 a) = bit1 (natAbs a)
[PROOFSTEP]
apply Int.natAbs_bit1_nonneg h₁
