proposition: Lemma eq_infty x : (forall r, r%:E <= x) -> x = +oo.
proof: Proof. case: x => [x /(_ (x + 1)%R)|//|/(_ 0%R)//]. by rewrite EFinD addeC -lee_subr_addr// subee// lee_fin ler10. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed