**Next:**References

**Up:**Formalizing Constructive Real Analysis

**Previous:**Tactics

# Tactic Code

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`.