proposition: Lemma limf_esup_dnbhsN {R : realType} (f : R -> \bar R) (a : R) : limf_esup f a^' = limf_esup (fun x => f (- x)%R) (- a)%R^'.
proof: Proof. rewrite /limf_esup dnbhsN image_comp/=. congr (ereal_inf [set _ | _ in _]); apply/funext => A /=. rewrite image_comp/= -compA (_ : _ \o _ = idfun)// funeqE => x/=. by rewrite opprK. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule