proposition: Lemma eq_ninfty x : (forall r, x <= r%:E) -> x = -oo.
proof: Proof. move=> *; apply: (can_inj oppeK); apply: eq_infty => r. by rewrite leeNr -EFinN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed