proposition: Lemma maxBy_monotone{T: Type}: forall f (l1 l2: list T) currentMax currentBest, (forall x, In x l1 -> In x l2) -> f currentBest = currentMax -> f (maxBy f currentMax currentBest l1) <= f (maxBy f currentMax currentBest l2).
proof: Proof. intros. subst. pose proof (maxBy_In f l1 (f currentBest) _ eq_refl) as P. destruct P as [P | P]. - specialize (H _ P). eapply lowerbound_maxBy. 1: exact H. reflexivity. - rewrite P. eapply maxBy_at_least_currentMax. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality