proposition: Lemma maxBy_at_least_currentMax{T: Type}: forall (f: T -> nat) l currentMax currentBest, f currentBest = currentMax -> currentMax <= f (maxBy f currentMax currentBest l).
proof: Proof. induction l; intros; simpl in *. - lia. - subst. destruct (f currentBest <? f a) eqn: E. + apply Nat.ltb_lt in E. specialize (IHl (f a) _ eq_refl). lia. + apply Nat.ltb_ge in E. eapply IHl. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality