From 00f593f9361af73290443fce9b16cc0cbe9884f4 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 26 Sep 2019 22:59:01 +0200
Subject: Non-distributive lattice

---
 mathcomp/field/algebraics_fundamentals.v | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index b41d5ec..0a759e8 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -586,13 +586,8 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
       by rewrite v_gt0 /= -if_neg posNneg.
     by rewrite v_lt0 /= -if_neg -(opprK v) posN posNneg ?posN.
   have absE v: le 0 v -> abs v = v by rewrite /abs => ->.
-  pose QyNum : realLtMixin (Q y) :=
-    RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _).
-  pose QyOrder :=
-    OrderType
-      (DistrLatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum.
-  pose QyNumField := [numFieldType of NumDomainType QyOrder QyNum].
-  pose Ry := [realFieldType of [realDomainType of QyNumField]].
+  pose Ry := LtRealFieldOfField
+               (RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _)).
   have archiRy := @rat_algebraic_archimedean Ry _ alg_integral.
   by exists (ArchiFieldType Ry archiRy); apply: [rmorphism of idfun].
 have some_realC: realC.
-- 
cgit v1.2.3