Real Arithmetic in TLAPM. - Ovini V. W. Gunasekera; Andrew Sogokon; Antonios Gouglidis; Neeraj Suri (NFM, 2024)