Theorem: Lean4Axiomatic.Integer.lt_inc (Lean4Axiomatic/Integer/Order.lean)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ a < a + 1
Tactic:
apply lt_iff_neg_diff.mpr
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ Negative (a - (a + 1))

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ Negative (a - (a + 1))
Tactic:
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
State after:
ℕ : 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))

State before:
ℕ : 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))
Tactic:
apply AA.substFn (Rel.symm ‹a - (a + 1) ≃ -1›)
State after:
ℕ : 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 (-1)

State before:
ℕ : 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 (-1)
Tactic:
exact neg_one_negative
State after:
no goals