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

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ m₁ ⊖ n₁ ≤ m₂ ⊖ n₂ ↔ n₂ + m₁ ≤ m₂ + n₁
Tactic:
simp only [LE.le, Int.le]
State after:
m₁ n₁ m₂ n₂ : Nat
⊢ ((m₂ ⊖ n₂) - (m₁ ⊖ n₁)).NonNeg ↔ (n₂ + m₁).le (m₂ + n₁)

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ ((m₂ ⊖ n₂) - (m₁ ⊖ n₁)).NonNeg ↔ (n₂ + m₁).le (m₂ + n₁)
Tactic:
rw [mk_sub_mk, nonNeg_mk]
State after:
m₁ n₁ m₂ n₂ : Nat
⊢ n₂ + m₁ ≤ m₂ + n₁ ↔ (n₂ + m₁).le (m₂ + n₁)

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