fact: Definition ArgMax {B} (f : B -> A) : Ensemble B := fun b => forall b', op (f b') (f b).
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation