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