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

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