fact: Fixpoint seq_of_max (f : ℕ → ℕ) (l : ℕ) := match l with | O => f O | S k => Nat.max (f l) (seq_of_max f k) end.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove