Intuitionize logbgcd1irr

[jkingdon]

The pull request starts with a proof in iset.mm of logbgcd1irr (as stated in set.mm). This involves some intuitionizing but no big changes to the structure of the proof.

As we do with other proofs involving irrationality, however, the concept bifurcates into two - the one that corresponds to logbgcd1irr we call "not rational" and the other one is being apart from any rational number, which we call "irrational" (I've also seen "strongly irrational" but I don't think that is common terminology).

Therefore, the pull request also includes logbgcd1irrap which is for irrational rather than not rational.

Includes:

• copying anim1ci , elpq , and elpqb from set.mm to iset.mm
• Several apartness theorems which are analogous to ones we have for operations like addition and multiplication. Although these are as general as I could quickly see how to make them, they are basically what I needed for logbgcd1irrap rather than trying to prove theorems of this sort for other future situations. They are: apexp1 , reapef, and apcxp2.

[jkingdon]

I had accidentally pushed up a few changes which weren't supposed to be on this branch but I undid that. This pull request is supposed to be logbgcd1irr and logbgcd1irrap (and a few things which lead up to those), nothing beyond that.