This is an equivalent to real trichotomy. Expand comment of trilpo to say more about equivalents to trichotomy.
Also prove trirec0xor which is the same as trirec0 but with exclusive-or (as stated in the discrete field definition at https://ncatlab.org/nlab/show/field ).
This is an equivalent to real trichotomy. Expand comment of trilpo to say more about equivalents to trichotomy.
Also prove trirec0xor which is the same as trirec0 but with exclusive-or (as stated in the discrete field definition at https://ncatlab.org/nlab/show/field ).
The larger context of this pull request is the discussion of analytic LPO at https://ncatlab.org/nlab/show/principle+of+omniscience#analytic