Algorithmic theory of rational numbers
Z Lem
Theorem. Axioms of ordered field and algorithmic formula saying for all n and m the Euclid's algorithm terminates uniquely determine the structure of rational numbers.
For the proof consult Antoni Kreczmar. Programmability in Fields. „Fundamenta Informaticae”, s. 195-230, 1977.