fact: Definition find_UpperBound (f : A -> nat) (ns : list A) : list A := let max := fold_right (fun n acc => max (f n) acc) O ns in filter (fun n => Nat.leb max (f n)) ns.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation