FOM: conics

[Matthew Frank]

> We assumed not(E=P), derived a contradiction, and concluded E=P.
> Do intuitionist geometers allow this?

This is either OK as it stands or works with a mild recasting:
Instead of getting a contradiction from not(E=P), we can get a
contradiction from dist(E,P)>epsilon.  Therefore dist(E,P) < 2 epsilon.
This since holds for every epsilon, dist(E,P)=0 and E=P.

In general, the use of trichotomy can be constructively justified whenever
deriving equalities or inclusive inequalities (like "less than or equal
to").  This is more or less because equalities and inclusive inequalities
are constructively equivalent to their own double negations, and because
the double negation of trichotomy is constructively provable.

Moral:  We may have difficulty sharpening our intuitions about what is
elementary, but at least technical work in f.o.m. makes it much easier to
sharpen our intuitions about what is constructive!

--Matt