Explain convert ... using in C03S06

[yannickseurin]

Section 3.6 introduces the convert tactic, but does not explain the convert ... using syntax. It is used in the proof of theorem convergesTo_mul towards the end of the section.

Arguably at this point of the book the reader has probably learned to use VSC overlays to look up what it means, but a sentence or two in the book would be helpful.