diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-26 12:13:06 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-26 12:13:06 +0000 |
| commit | 4aec8fda1161953cf929b4e282eea9b672ab4058 (patch) | |
| tree | eea4b8ab24fdea8fb05206b1764ce1ed3c752d72 /theories/Reals/RIneq.v | |
| parent | 351a500eada776832ac9b09657e42f5d6cd7210f (diff) | |
commit de field + renommages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/RIneq.v')
| -rw-r--r-- | theories/Reals/RIneq.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 3b5d241fa..c6feb4ac6 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -13,9 +13,9 @@ (***************************************************************************) Require Export Raxioms. -Require Export NewZArithRing. +Require Export ZArithRing. Require Import Omega. -Require Export Field_tac. Import NewField. +Require Export Field_tac. Import Field. Open Local Scope Z_scope. Open Local Scope R_scope. @@ -88,7 +88,7 @@ apply Rlt_trans with (0 + 1). apply Rplus_0_l. Qed. -Lemma Rgen_phiPOS : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x > 0. +Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0. unfold Rgt in |- *. induction x; simpl in |- *; intros. apply Rlt_trans with (1 + 0). @@ -111,7 +111,8 @@ induction x; simpl in |- *; intros. Qed. -Lemma Rgen_phiPOS_not_0 : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x <> 0. +Lemma Rgen_phiPOS_not_0 : + forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0. red in |- *; intros. specialize (Rgen_phiPOS x). rewrite H in |- *; intro. @@ -119,8 +120,8 @@ apply (Rlt_asym 0 0); trivial. Qed. Lemma Zeq_bool_complete : forall x y, - ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp x = - ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp y -> + InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x = + InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y -> Zeq_bool x y = true. Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0. |