have : a - (a + 1) ≃ -1 := calc
  a - (a + 1)   ≃ _ := sub_defn
  a + -(a + 1)  ≃ _ := AA.substR neg_compat_add
  a + (-a + -1) ≃ _ := Rel.symm AA.assoc
  (a + -a) + -1 ≃ _ := AA.substL AA.inverseR
  (0 : ℤ) + -1  ≃ _ := AA.identL
  (-1)          ≃ _ := Rel.refl
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ Negative (a - (a + 1))
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
this : a - (a + 1) ≃ -1
⊢ Negative (a - (a + 1))