proposition: Lemma gee0P x : 0 <= x <-> x = +oo \/ exists2 r, (r >= 0)%R & x = r%:E.
proof: Proof. split=> [|[->|[r r0 ->//]]]; last by rewrite real_leey/=. by case: x => [r r0 | _ |//]; [right; exists r|left]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed