fact: Definition MaxElements (elements : Comp (list A)) := elements' <- elements; ⟦ element in elements' | UpperBound elements' element ⟧.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation