如何针对nat类型变量应用ssralg的addf_div定理化简分式？

首先必须明确：要让分母a%:R有意义，需要假设a ≠ 0（nat类型的a不为0，对应实数域中a%:R ≠ 0%:R），否则分式无定义。

接下来，R（实数域）本身就是fieldType的实例，所以只要把目标中的表达式明确对应到R域内的运算，就能直接应用addf_div定理。具体操作步骤如下：

1. 明确类型转换：把目标里的1、2都显式转换为实数域元素，即1%:R、2%:R，此时目标变为：

   1%:R / a%:R + 1%:R / a%:R = 2%:R / a%:R
   

2. 应用addf_div定理：addf_div的核心逻辑是「同分母分式相加，分母不变分子相加」，它的类型是forall (F : fieldType) (x y z : F), z != 0 -> x/z + y/z = (x + y)/z。这里F取R，x = 1%:R，y = 1%:R，z = a%:R，且由a ≠ 0可推出z != 0，直接应用定理后，目标变为：

   (1%:R + 1%:R) / a%:R = 2%:R / a%:R
   

3. 化简分子：利用实数域内的加法规则，1%:R + 1%:R = 2%:R，直接化简即可完成证明。

在Coq证明脚本中的具体写法示例：

From mathcomp Require Import ssralg reals.

Lemma example (a : nat) : a ≠ 0 -> 1 / a%:R + 1 / a%:R = 2 / a%:R.
Proof.
move => Ha.
rewrite !/(1 / a%:R) /=; (* 显式展开分式，明确类型为R域内运算 *)
rewrite addf_div; first by rewrite -(natr_neq0 Ha). (* 应用addf_div，同时证明分母非零 *)
rewrite add1r; (* 化简1%:R + 1%:R为2%:R *)
by rewrite /(2 / a%:R) /=; (* 统一形式完成证明 *)
Qed.

注：natr_neq0是math-comp中用于将nat的非零性质转换为对应实数非零的定理，add1r是实数域内1加1等于2的定理（或直接用addnC结合nat到R的coercion性质）。

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