this : 1 ≠ -1
⊢ ∀ {m n : ℤ}, sign m = sign n → sign (m + n) = sign n
⊢ ∀ {m n : ℤ}, sign m = sign n → sign (m + n) = sign n
have : (1 : ℤ) ≠ -1 := by decide
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ sign (↑m + 1 + (↑n + 1)) = 1
this : 1 ≠ -1
⊢ ∀ {m n : ℤ}, sign m = sign n → sign (m + n) = sign n
rintro ((_ | m) | m) ((_ | n) | n) <;> simp [this, this.symm]
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑m + 1 + (↑n + 1)
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ sign (↑m + 1 + (↑n + 1)) = 1
rw [Int.sign_eq_one_iff_pos]
no goals
⊢ 1 ≠ -1
decide
no goals
case ofNat.succ.ofNat.succ.hb
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑n + 1
exact zero_lt_one.trans_le (le_add_of_nonneg_left <| coe_nat_nonneg _)