The tactics described above, together with some special-purpose lemmas to which they refer.
For readability, different notations have been used in the following theorems. a. is the rational number a/1.
Again we use some more visible notation. a
is the real number
i.a.
