如何将nat类型的a%:R转为域类型以使用unitfE求解单位元目标？

• 核心思路是通过类型转换将自然数a映射到域类型，再关联到R类型，从而适配unitfE引理：

  1. 用of_nat将nat类型的a转换为域类型（比如real），得到of_nat a；
  2. 若R是域的实例，用对应转换函数（如of_real）将域类型值转成R类型，此时目标可改写为(of_real (of_nat a))%:R \is a unit；
  3. 直接调用unitfE引理完成证明——该引理针对域中的单位元判定，通常等价于“值不为0”；
  4. 若R是real的别名，可配合simp将目标简化为a ≠ 0，因为自然数转实数非0当且仅当原自然数非0。

• 示例证明片段：

lemma "a%:R \is a unit"
proof -
  assume "a ≠ 0"
  then have "of_nat a ≠ 0" by simp
  then have "(of_real (of_nat a))%:R \is a unit" by (rule unitfE)
  then show ?thesis by (simp add: of_nat_of_real_eq)
qed

内容的提问来源于stack exchange，提问作者dvr