proposition: Lemma ereal_nondecreasing_oppn u_ : nondecreasing_seq (-%E \o u_) = nonincreasing_seq u_.
proof: Proof. rewrite propeqE; split => ni_u m n mn; last by rewrite leeNr oppeK ni_u. by rewrite -(oppeK (u_ m)) -leeNr ni_u. 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