proposition: Lemma Sup_fct_bound (f : R -> R) (a b : R) : Sup_fct f a b = Sup_fct f b a.
proof: Proof. rewrite /Sup_fct /= ; case: Req_EM_T => Hab ; case: Req_EM_T => Hba. by []. by apply sym_equal in Hab. by apply sym_equal in Hba. apply Lub_Rbar_eqset => x ; by rewrite Rmin_comm Rmax_comm. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy