mise a jour du nouveau ring et ajout du nouveau field, avant renommages

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 13 deletions

diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index e4b22dd56..5b4d8db03 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -52,8 +52,9 @@ assert ((X1 * Y2)%R = (Y1 * X2)%R).
  unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR.
  apply IZR_eq; auto.
 clear H.
-field; auto.
-rewrite <- H0; field; auto.
+field_simplify_eq; auto.
+ring_simplify X1 Y2 (Y2 * X1)%R.
+rewrite H0 in |- *;  ring.
 Qed.
 
 Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.
@@ -176,16 +177,11 @@ unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
 case x1.
 simpl in |- *; intros; elim H; trivial.
 intros; field; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rinv_neq_0_compat; auto.
-intros; field; auto.
-do 2 rewrite <- mult_IZR.
-simpl in |- *; rewrite Pmult_comm; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply not_O_IZR; auto with qarith.
-apply Rinv_neq_0_compat; auto.
+intros; 
+  change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *;
+  change (IZR (Zneg p)) with (- IZR (' p))%R in |- *;
+  field; (*auto 8 with real.*)
+  repeat split; auto; auto with real.
 Qed.
 
 Lemma Q2R_div :
@@ -210,4 +206,4 @@ Goal forall x y : Q, ~ y==0#1 -> (x/y)*y == x.
 intros; QField.
 intro; apply H; apply eqR_Qeq.
 rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real.
-Abort.
\ No newline at end of file
+Abort.