[GOAL]
m n : ℕ
⊢ ↑m - ↑n ≤ ↑(m - n)
[PROOFSTEP]
by_cases h : m ≥ n
[GOAL]
case pos
m n : ℕ
h : m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)
[PROOFSTEP]
exact le_of_eq (Int.ofNat_sub h).symm
[GOAL]
case neg
m n : ℕ
h : ¬m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)
[PROOFSTEP]
simp [le_of_not_ge h, ofNat_le]
[GOAL]
n : ℕ
⊢ 0 ≤ ↑n
[PROOFSTEP]
simp
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
[PROOFSTEP]
rw [sq, sq]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a = natAbs b ↔ a * a = b * b
[PROOFSTEP]
exact natAbs_eq_iff_mul_self_eq
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
[PROOFSTEP]
rw [sq, sq]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a < natAbs b ↔ a * a < b * b
[PROOFSTEP]
exact natAbs_lt_iff_mul_self_lt
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2
[PROOFSTEP]
rw [sq, sq]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
⊢ natAbs a ≤ natAbs b ↔ a * a ≤ b * b
[PROOFSTEP]
exact natAbs_le_iff_mul_self_le
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ natAbs a = natAbs b ↔ a = b
[PROOFSTEP]
rw [← sq_eq_sq ha hb, ← natAbs_eq_iff_sq_eq]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ natAbs a = natAbs b ↔ a = b
[PROOFSTEP]
simpa only [Int.natAbs_neg, neg_inj] using
  natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) (neg_nonneg_of_nonpos hb)
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : 0 ≤ a
hb : b ≤ 0
⊢ natAbs a = natAbs b ↔ a = -b
[PROOFSTEP]
simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg ha (neg_nonneg_of_nonpos hb)
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ natAbs a = natAbs b ↔ -a = b
[PROOFSTEP]
simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) hb
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a : ℤ
x✝ : a ∈ Iic 0
b : ℤ
hb : b ∈ Iic 0
hab : a < b
⊢ natAbs b < natAbs a
[PROOFSTEP]
simpa [Int.natAbs_neg] using natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)
[GOAL]
a b : ℤ
n✝ n : ℕ
h : ↑(n + 1) ≤ 0
⊢ 0 < ↑(n + 1)
[PROOFSTEP]
simp
[GOAL]
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ div2 (bit b n) = n
[PROOFSTEP]
rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]
[GOAL]
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0
case H a b✝ : ℤ n✝ : ℕ b : Bool n : ℤ ⊢ 2 ≠ 0
[PROOFSTEP]
cases b
[GOAL]
case false
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0
[PROOFSTEP]
simp
[GOAL]
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0
[PROOFSTEP]
show ofNat _ = _
[GOAL]
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ ofNat (1 / 2) = 0
[PROOFSTEP]
rw [Nat.div_eq_zero]
[GOAL]
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ ofNat 0 = 0
[PROOFSTEP]
simp
[GOAL]
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ 1 < 2
[PROOFSTEP]
simp
[GOAL]
case H
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ 2 ≠ 0
[PROOFSTEP]
decide
