for n being Nat holds Euclid n is complete by Th13;