From 21ed2bfa901108d69893bc8480d215edeb255d6d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 19 Feb 2021 19:29:46 +0100
Subject: Abstract the non-computational part away.

---
 theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
index a180e13444..bc45868244 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
@@ -733,13 +733,11 @@ Definition CReal_inv_pos (x : CReal) (Hxpos : 0 < x) : CReal :=
   bound := CReal_inv_pos_bound x Hxpos
 |}.
 
-(* ToDo: make this more obviously computing *)
-
 Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x.
 Proof.
   intros x [n nmaj]. exists n.
-  apply (Qlt_le_trans _ _ _ nmaj). destruct x. simpl.
-  unfold Qminus. rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl.
+  simpl in *. unfold CReal_opp_seq, Qminus.
+  abstract now rewrite Qplus_0_r, <- (Qplus_0_l (- seq x n)).
 Defined.
 
 Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal
-- 
cgit v1.2.3