proposition: Lemma lowerbound_maxBy{T: Type}: forall (f: T -> nat) x l currentMax currentBest, List.In x l -> f currentBest = currentMax -> f x <= f (maxBy f currentMax currentBest l).
proof: Proof. induction l; intros; simpl in *. - contradiction. - destruct H. + subst. destruct (f currentBest <? f x) eqn: E. * apply Nat.ltb_lt in E. eapply maxBy_at_least_currentMax. reflexivity. * apply Nat.ltb_ge in E. eapply Nat.le_trans. 1: eassumption. eapply maxBy_at_least_currentMax. reflexivity. + subst. destruct (f currentBest <? f a) eqn: E. * apply Nat.ltb_lt in E. eauto. * apply Nat.ltb_ge in E. eauto. Qed.
imports: Arith Lia List FunctionalExtensionality