47. Clamp never goes below the bound
clamp lo n returns lo when n < lo and n otherwise. Prove lo ≤ clamp lo n for every lo and n.
No hypothesis tells you which branch runs, so the proof has to handle both.
1def clamp (lo n : Nat) : Nat := if n < lo then lo else n
2theorem solution (lo n : Nat) : lo ≤ clamp lo n := by
givenLoading editor…
Type
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
lo n:Nat
⊢lo ≤ clamp lo n
ReadyLn 1, Col 1Lean 4
Draft saved in this browser