From ad0c122b1665fedde52f51ecdebb9d04a12831a6 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 24 Jun 2011 15:50:17 +0000 Subject: Clean-up of Znumtheory, deletion of Zgcd_def In particular, we merge the old Zdivide (used to be an ad-hoc inductive predicate) and the new Z.divide (based on exists). Notations allow to do that (almost) transparently, the only impact is that the name picked by the system will not be "q" anymore when destructing a Z.divide. Some fragile scripts may have to be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14239 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/QArith/Qreduction.v | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) (limited to 'theories/QArith') diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 4888ce4b1..e39eca0cb 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -9,7 +9,7 @@ (** Normalisation functions for rational numbers. *) Require Export QArith_base. -Require Import Zgcd_def Znumtheory. +Require Import Znumtheory. (** First, a function that (tries to) build a positive back from a Z. *) @@ -83,14 +83,13 @@ Proof. exists bb; auto with zarith. intros. inversion Hg1. - destruct (H6 (g*x)). + destruct (H6 (g*x)) as (x',Hx). rewrite Hg3. destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring. rewrite Hg4. destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring. - exists q. - apply Zmult_reg_l with g; auto. - pattern g at 1; rewrite H7; ring. + exists x'. + apply Zmult_reg_l with g; auto. rewrite Hx at 1; ring. (* /rel_prime *) unfold rel_prime in |- *. (* rel_prime *) @@ -99,14 +98,13 @@ Proof. exists dd; auto with zarith. intros. inversion Hg'1. - destruct (H6 (g'*x)). + destruct (H6 (g'*x)) as (x',Hx). rewrite Hg'3. destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring. rewrite Hg'4. destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring. - exists q. - apply Zmult_reg_l with g'; auto. - pattern g' at 1; rewrite H7; ring. + exists x'. + apply Zmult_reg_l with g'; auto. rewrite Hx at 1; ring. (* /rel_prime *) assert (0