Editing Constructive analysis (section)

====Non-strict partial order====
Lastly, the relation <math>0\ge x</math> may be defined by or proven equivalent to the '''logically negative''' statement <math>\neg(x > 0)</math>, and then <math>x \le 0</math> is defined as <math>0 \ge x</math>. Decidability of positivity may thus be expressed as <math>x > 0\lor 0\ge x</math>, which as noted will not be provable in general. But neither will the totality disjunction <math>x\ge 0 \lor 0\ge x</math>, see also [[limited principle of omniscience|analytical <math>{\mathrm {LLPO}}</math>]].

By a valid [[De Morgan's laws#In intuitionistic logic|De Morgan's law]], the conjunction of such statements is also rendered a negation of apartness, and so
:<math>(x\ge y \land y\ge x)\leftrightarrow (x\cong y)</math>
The disjunction <math>x > y \lor x\cong y</math> implies <math>x\ge y</math>, but the other direction is also not provable in general. In a constructive real closed field, '''the relation "<math>\ge</math>" is a negation and is not equivalent to the disjunction in general'''.