proposition: Lemma esupsN u : esups (-%E \o u) = -%E \o einfs u.
proof: Proof. rewrite funeqE => n; rewrite /esups /= oppeK; congr (ereal_sup _). by rewrite predeqE => x; split => [[m /= nm <-]|[_ [m /= nm] <-] <-]; [exists (u m) => //; exists m | exists m]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau