[Python-ideas] Re: Make 10**400 / 1e200 work?