Theorem: useful_fact (LeanCourse/Assignments/Assignment2.lean)

State before:
s t : ℕ → ℕ
k a b c : ℕ
⊢ c ≥ max a b ↔ c ≥ a ∧ c ≥ b
Tactic:
simp
State after:
no goals