proposition: Lemma Inf_fct_bound (f : R -> R) (a b : R) : Inf_fct f a b = Inf_fct f b a.
proof: Proof. rewrite /Inf_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 Glb_Rbar_eqset => x ; by rewrite Rmin_comm Rmax_comm. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy