Relationships between inequality, strict inequality, and their negations on reals

[lowasser]

I haven't yet bothered with the theorems that require LEM -- or at least truncated LEM, which I don't yet understand the equivalence of with LEM -- but these results are tractable.

[EgbertRijke]

If P is a proposition, then is-decidable (type-Prop P) is already a proposition, as was shown here:

is-decidable-Prop

So, propositionally truncating it results simply in an equivalent proposition. I suspect that you needed proposition in a place where you would have liked to use is-decidable (type-Prop P), and thought that the solution must have been to propositionally truncate it. Luckily, however, you have is-decidable-Prop P at your disposal.

[fredrik-bakke]

Nice additions! I only have some stylistic changes I'd like you to implement before this is merged.

[lowasser]

I think we're done? I do prefer "less than" and "less than or equal to" to "strictly less than" and "less than."