a b c : Nat
x✝ : a ≤ c ∧ b ≤ c
h₁ : a ≤ c
h₂ : b ≤ c
⊢ (if a ≤ b then b else a) ≤ c
a b c : Nat
x✝ : a ≤ c ∧ b ≤ c
h₁ : a ≤ c
h₂ : b ≤ c
⊢ max a b ≤ c
rw [Nat.max_def]
no goals
a b c : Nat
x✝ : a ≤ c ∧ b ≤ c
h₁ : a ≤ c
h₂ : b ≤ c
⊢ (if a ≤ b then b else a) ≤ c
split <;> assumption