proposition: Lemma refine_FindUpperBound {A B} : forall (op : B -> B -> Prop) (op_trans : forall b b' b'', op b b' -> op b' b'' -> op b b'') (bound : B) (As As' : list A) (f : A -> B), (forall a, List.In a As' -> op (f a) bound) -> (exists a, List.In a As' /\ f a = bound) -> refine (⟦element in As | UpperBound (fun a a' => op (f a) (f a')) As' element ⟧) (⟦element in As | op bound (f element) ⟧).
proof: Proof. intros. unfold UpperBound. apply refine_ListComprehension_Equiv. split; intros. - destruct H0; intuition eauto; subst; eauto. - eapply op_trans; eauto. Qed.
imports: Coq.Arith.Arith Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common.DecideableEnsembles Fiat.Computation