fact: Definition UpperBound (rs : list A) (r : A) := forall r' : A, List.In r' rs -> op r' r.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation