Next: References Up: Formalizing Constructive Real Analysis Previous: Tactics
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.