proposition: Lemma nonincreasing_at_right_cvge (f : R -> \bar R) a (b : itv_bound R) : (BRight a < b)%O -> {in Interval (BRight a) b &, nonincreasing_fun f} -> f x @[x --> a ^'+] --> ereal_sup (f @` [set` Interval (BRight a) b]).
proof: Proof. move=> ab nif; have ndNf : {in Interval (BRight a) b &, {homo (\- f) : n m / (n <= m)%R >-> n <= m}}. by move=> r s rab sab /nif; rewrite leeN2; exact. have /cvgeN := nondecreasing_at_right_cvge ab ndNf. under eq_fun do rewrite oppeK. set lhs := (X in _ --> X -> _); set rhs := (X in _ -> _ --> X). suff : lhs = rhs by move=> ->. rewrite {}/rhs {}/lhs; rewrite /ereal_inf oppeK; congr ereal_sup. by rewrite image_comp/=; apply: eq_imagel => x _ /=; rewrite oppeK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)