From 351a500eada776832ac9b09657e42f5d6cd7210f Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 26 Sep 2006 11:18:22 +0000 Subject: 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 --- theories/QArith/Qreals.v | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) (limited to 'theories/QArith/Qreals.v') 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. -- cgit v1.2.3