Hi Ed,
5V/4096=1.2207mV per count. You can use the ** operator to multiply by units of 1/65536, try something like Voltage = ADResult ** 8000.
Basically the ** operator multiplies by the value given and then divides the intermediate 32bit result by 65536 so doing ADResult ** 8000 would be the same as doing ADResult / 0.12207 if you could do that.

At 5V input you'll get a ADResult of 4096. 4096*8000/65536=500 representing 5.00V
At 3.71V input you'll get an ADResult of 3040. 3040*8000/65536=371 representing 3.71V

It's not perfect bu pretty close. How I came up with 8000? Because 500/4096 * 65536 = 8000

/Henrik.