I am trying to prove this :

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

```

This is what I've done so far :

```ml
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.

```

With the current goal being :

```ml
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

```

Given `absurd_ineq : 1 <= / 2`, how can I tell Coq that this comparison evaluates to `False`, in order to then use the `contradiction` tactic ?

I have tried using `vm_compute` and `cbv` in hope that `absurd_ineq` is simplified, evaluated, to `False`, but no chance.

Thanks.

EDIT :
The statement `forall a : R, (forall e : R, e > 0 /\ Rabs a <= e) -> a = 0` wasn't the right one, `forall a : R, (forall e : R, e > 0 -> Rabs a <= e) -> a = 0` was.

Here's the proof :

```ml
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.```

```