proposition: Lemma find_UpperBound_highest_length : forall (f : A -> nat) ns n, List.In n (find_UpperBound f ns) -> forall n', List.In n' ns -> (f n) >= (f n').
proof: Proof. unfold ge, find_UpperBound; intros. apply filter_In in H; destruct H. apply Nat.leb_le in H1. rewrite <- H1; clear H1 H n. apply fold_right_max_is_max; auto. Qed.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation