Theorem: Int.mk_lt_mk (Extra/Int/Lemmas.lean)

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ m₁ ⊖ n₁ < m₂ ⊖ n₂ ↔ n₂ + m₁ < m₂ + n₁
Tactic:
simp only [LT.lt, Int.lt, Nat.lt]
State after:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) + 1 ≤ m₂ ⊖ n₂ ↔ (n₂ + m₁).succ.le (m₂ + n₁)

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) + 1 ≤ m₂ ⊖ n₂ ↔ (n₂ + m₁).succ.le (m₂ + n₁)
Tactic:
rw [←one_mk_zero, mk_add_mk, mk_le_mk, Nat.add_succ, Nat.add_zero]
State after:
m₁ n₁ m₂ n₂ : Nat
⊢ (n₂ + m₁).succ ≤ m₂ + n₁ ↔ (n₂ + m₁).succ.le (m₂ + n₁)

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ (n₂ + m₁).succ ≤ m₂ + n₁ ↔ (n₂ + m₁).succ.le (m₂ + n₁)
Tactic:
rfl
State after:
no goals