From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 theories/Reals/LegacyRfield.v | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 theories/Reals/LegacyRfield.v

(limited to 'theories/Reals/LegacyRfield.v')

diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
new file mode 100644
index 00000000..b33274af
--- /dev/null
+++ b/theories/Reals/LegacyRfield.v
@@ -0,0 +1,40 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Raxioms.
+Require Export LegacyField.
+Import LegacyRing_theory.
+
+Section LegacyRfield.
+
+Open Scope R_scope.
+
+Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
+  split.
+  exact Rplus_comm.
+  symmetry  in |- *; apply Rplus_assoc.
+  exact Rmult_comm.
+  symmetry  in |- *; apply Rmult_assoc.
+  intro; apply Rplus_0_l.
+  intro; apply Rmult_1_l.
+  exact Rplus_opp_r.
+  intros.
+  rewrite Rmult_comm.
+  rewrite (Rmult_comm n p).
+  rewrite (Rmult_comm m p).
+  apply Rmult_plus_distr_l.
+  intros; contradiction.
+Defined.
+
+End LegacyRfield.
+
+Add Legacy Field
+R Rplus Rmult 1%R 0%R Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
+  with minus := Rminus div := Rdiv.
-- 
cgit v1.2.3