запросить разъяснения относительно появления очевидного реального принуждения в теории натуральных чисел в теории Изабель

Я изучаю следующую теорию в Isabelle2020 / jEdit:

theory Sqrt
imports Complex_Main "HOL-Computational_Algebra.Primes"
begin

theorem
  assumes "prime (p::nat)"
  shows "sqrt p ∉ ℚ"
proof
  from ‹prime p› have p: "1 < p" by (simp add: prime_nat_iff)
  assume "sqrt p ∈ ℚ"
  then obtain m n :: nat where
      n: "n ≠ 0" and sqrt_rat: "¦sqrt p¦ = m / n"
    and "coprime m n" by (rule Rats_abs_nat_div_natE)

[we omit the remainder of the proof]

Панель вывода показывает состояние проверки:

have (⋀m n. n ≠ 0 ⟹ ¦sqrt (real p)¦ = real m / real n ⟹ coprime m n ⟹ ?thesis) ⟹ ?thesis 
proof (state)
this:
    n ≠ 0
    ¦sqrt (real p)¦ = real m / real n
    coprime m n

goal (1 subgoal):
 1. sqrt (real p) ∈ ℚ ⟹ False

У меня вопрос: являются ли эти видимости реальными принуждением типа? Я прочитал главу 8, в которой обсуждаются типы в так называемом учебнике, прилагаемом к дистрибутиву Isabelle (заголовок «Помощник по доказательству для логики высшего порядка»). Я прочитал заголовок документа Флориана Хафтмана Isabelle / HOL type-class hierarchy (также часть распределения Isabelle). Правило, используемое в приведенных выше утверждениях теории, Rats_abs_nat_div_natE, является леммой в Real.thy теории.

Я поискал ссылку в этом файле теории и посмотрел на §8.4.5 в Помощник по доказательству для логики высшего порядка, где обнаружил, что тип натурального числа nat является линейно упорядоченным полукольцом, тип int - упорядоченное кольцо, а тип real - это упорядоченное поле. Свойства могут не соблюдаться для определенного класса, например, для типа nat не удерживаются абстрактные свойства, включающие вычитание (поскольку, конечно, можно получить отрицательное число, которое не будет натуральным числом). Вместо этого приводятся конкретные теоремы, касающиеся вычитания типа nat. Более того, «все абстрактные свойства, включающие деление, требуют поля. (Помощник по проверке логики высшего порядка.)

Итак, мы видим здесь факторный тип, используемый для поднятия деления натуральных или целочисленных типов на абстрактный реальный тип, чтобы удовлетворить требованиям поля (см. §11.9 Справочное руководство Isabelle / Isar )? Факторный тип real создается из определения отношения эквивалентности realrel в файле Real.thy.

Я был удивлен, увидев в доказательстве вещественные члены, зависящие от простых, целых положительных и рациональных чисел, и хотел заверить, что, по крайней мере, приблизился к объяснению того, почему это происходит в доказательстве Изабель.