Coq实数证明中如何判定常数不等式为假导出矛盾

我在证明实数相关命题时遇到了卡点：
最初编写的待证命题如下：

Goal forall a : R, (forall e : R, e > 0 /\ Rabs a <= e) -> a = 0.

已编写的部分证明代码：

Goal forall a : R, (forall e : R, e > 0 /\ Rabs a <= e) -> a = 0.
Proof.
  intros a H.
  destruct (classic (a = 0)) as [a_eq_0 | a_neq_0].

  - trivial.
  - apply (Rabs_pos_lt a) in a_neq_0 as Rabs_a_gt_0.
    pose (e := Rabs a / 2).
    cut (Rabs a <= e).

    * intro absurd_ineq.
      cbv [e] in absurd_ineq.
      apply (Rmult_le_compat_r (/(Rabs a))) in absurd_ineq.
      unfold Rdiv in absurd_ineq.
      rewrite (Rinv_r (Rabs a) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.
      rewrite (Rinv_r_simpl_m (Rabs a) (/2) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.

执行到此处时证明卡住，当前子目标状态：

2 goals
  
  a : R
  H : forall e : R, e > 0 /\ Rabs a <= e
  a_neq_0 : a <> 0
  Rabs_a_gt_0 : 0 < Rabs a
  e := Rabs a / 2 : R
  absurd_ineq : 1 <= / 2
  ============================
  a = 0

goal 2 is:
 0 <= / Rabs a

我尝试过用vm_compute、cbv策略化简假设absurd_ineq : 1 <= / 2，希望将其化简为False后用contradiction完成证明，但没有达到预期效果，需要找到正确的方法从该矛盾假设导出结论。

• 计算类策略无法处理公理化实数的判定
  Coq标准库的实数类型R是公理化定义的，不是可计算的归纳类型，vm_compute、cbv这类基于项求值的策略无法对公理化的实数运算、序关系做化简，因此无法直接识别该不等式为假。
• 使用lra策略自动判定线性实数算术命题
  lra是Coq内置的线性实数算术自动化判定策略，内置了实数域上序关系、加减、常数乘除相关的公理和判定规则，可以直接识别1 <= /2（即1 <= 1/2）为矛盾命题导出False，同时也能自动解决第二个子目标0 <= / Rabs a（上下文已经证明Rabs a > 0，其倒数自然非负），不需要手动做矛盾推导。

最初的命题陈述存在书写错误：原命题将“对任意大于0的e，都有Rabs a <= e”错误写为了合取形式e > 0 /\ Rabs a <= e，正确的命题应该是蕴含形式。修正命题后完整可运行的证明代码如下：

Goal
  forall a : R, (forall e : R, e > 0 -> Rabs a <= e) -> a = 0.
Proof.
  intros a H.
  destruct (classic (a = 0)) as [a_eq_0 | a_neq_0].

  - trivial.
  - apply (Rabs_pos_lt a) in a_neq_0 as Rabs_a_spos.
    pose (e := Rabs a / 2).
    cut (Rabs a <= e).

    * intro absurd_ineq.
      cbv [e] in absurd_ineq.
      apply (Rmult_le_compat_r (/(Rabs a))) in absurd_ineq; [| lra].
      unfold Rdiv in absurd_ineq.
      rewrite (Rinv_r (Rabs a) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.
      rewrite (Rinv_r_simpl_m (Rabs a) (/2) (Rabs_no_R0 a a_neq_0)) in absurd_ineq.
      lra.
    * specialize (H e).
      apply Rlt_gt in Rabs_a_spos.
      apply Rgt_ge in Rabs_a_spos as Rabs_a_pos.
      cbv [e] in *.
      lra.
Qed.

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