proposition: Lemma maxBy_In{T: Type}: forall f (l: list T) currentMax currentBest, currentMax = f currentBest -> List.In (maxBy f currentMax currentBest l) l \/ maxBy f currentMax currentBest l = currentBest.
proof: Proof. induction l; intros. - simpl. auto. - subst. simpl in *. destruct (f currentBest <? f a) eqn: E. + specialize (IHl (f a) _ eq_refl). firstorder congruence. + specialize (IHl (f currentBest) _ eq_refl). firstorder congruence. Qed.
imports: Arith Lia List FunctionalExtensionality