Simplification in Semi-continuous real ? Hi !
I'm considering in a general topos $T$ the object $R$ of lower semi-continuous real (one sided lower non-empty Dedekind cuts, as for exemple in http://ncatlab.org/nlab/show/one-sided+real+number ).
I want to know if, even if substraction is not possible, there is (internally) some sort of simplification rules for addition like :
If $x$ is 'bounded' (there exist a rational q such that $x \leqslant q$ ) then $x+a=x+b$ imply $a=b$.
It's seem true to me, but only because of an argument involving a covering of $T$ by a boolean topos, if it's possible I would prefer a completely internal argument, and I can't find it.
[Edited by Andrej Bauer] A lower Dedekind cut is a subset $L \subseteq \mathbb{Q}$ which is


*

*rounded: $q \in L \iff \exists r \in L . q < r$

*inhabited $\exists q \in \mathbb{Q} . q \in L$

*bounded: $\exists q \in \mathbb{Q} \forall r \in L . r < q$

 A: Ok I think I finally found an internaly valid proof by my self, so I explain it briefly here in case someone is interested some day :
If $U \in \Omega$ is a subterminal object, you can define the element $1_U \in R$ as :
$q \in 1_U$ when $q < 0 \cup (U \cap q<1)$.
(this correspond to the indicator function of an open set... )
It's easy to show that if $x+1_U \leqslant y + 1_U$ then $x \leqslant y$ :
if $q < x$, then $q < x+1_U$, hence, $\exists u,v$ such that $q=u+v, u < y$ and $v < 0 \cup (v<1 \cap U)$


*

*First case : $v<0$ then, $q < u < y$, we have $q < y$.

*Second case : we have 'U' then $1_U = 1$ so $q+1 < x+1_U$, 
$q+1 < y +1$
$q < y$
In both case, $q < y$ so $x \leqslant y$.
Now, if $x$ is any bounded positive element, let $N$ be an integer such that $x < N$.
on can define :
$\displaystyle h = \frac{1}{n} \sum_{i=1}^{N.n } 1_{x> (i/n)}  $
and one can show that (but it's a little longer) :
$h \leqslant x \leqslant h+\frac{1}{n}$.
It's now easy to conclude if $x$ is positive and bounded and $a + x \leqslant x + b$
then if $q < a$, take $q'$ another rational such that $q < q' < a$, let $n$ an integer such that $q'-q < \frac{1}{n}$. and let $h$ be as above :
$ a + h \leqslant a +x \leqslant b+x \leqslant b + h + 1/n $ 
but by a simple recurence, h can be simplified so :
$ a \leqslant b+1/n $
so $q' < b+1/n$, and finaly $q < q'-1/n < b $
If $x$ is not positive, just take some $q < x$, and $x-q$ will be positive
