Theorem: Int.ge_trans (MLIR/Util/Arith.lean)

State before:
n k m : ℤ
⊢ n ≥ m → m ≥ k → n ≥ k
Tactic:
simp [GE.ge]
State after:
n k m : ℤ
⊢ m ≤ n → k ≤ m → k ≤ n

State before:
n k m : ℤ
⊢ m ≤ n → k ≤ m → k ≤ n
Tactic:
intros h₁ h₂
State after:
n k m : ℤ
h₁ : m ≤ n
h₂ : k ≤ m
⊢ k ≤ n

State before:
n k m : ℤ
h₁ : m ≤ n
h₂ : k ≤ m
⊢ k ≤ n
Tactic:
apply le_trans h₂ h₁
State after:
no goals