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$