proposition: Lemma elements_le_seq_of_max : ∀ (g : ℕ → ℕ) (n : ℕ) (k : ℕ), (k ≤ n)%nat ⇒ (g k ≤ seq_of_max g n)%nat.
proof: Proof. Take g : (ℕ → ℕ). Take n : ℕ and k : ℕ; such that (k ≤ n)%nat. By elements_le_seq_of_max_pre it holds that (g k ≤ seq_of_max g k)%nat. We claim that (seq_of_max g k ≤ seq_of_max g n)%nat. { By incr_loc_to_glob it suffices to show that (is_increasing (seq_of_max g)). By seq_of_max_is_increasing we conclude that (is_increasing (seq_of_max g)). } We conclude that (& g k <= seq_of_max g k <= seq_of_max g n)%nat. Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove