apply le_max_right
case left
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ max N N' ≥ N'

case right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N
case right
φ : ℕ → ℕ
h : extraction φ
N N' : ℕ
⊢ φ (max N N') ≥ N