In agreement with Laurent Thery, start migration of auxiliary results

present in Ints. For the moment, mainly: 
 - Q parts go in QArith
 - Some of the Zdivide & Zgcd stuff go in Znumtheory

More to come ...



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

3 files changed, 56 insertions, 3 deletions

diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 959a16c29..cfe0187a3 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -547,4 +547,14 @@ auto.
 Qed.
 
 
-
+Theorem Qc_decomp: forall x y: Qc,
+  (Qred x = x -> Qred y = y -> (x:Q) = y)-> x = y.
+Proof.
+  intros (q, Hq) (q', Hq'); simpl; intros H.
+  assert (H1 := H Hq Hq').
+  subst q'.
+  assert (Hq = Hq'). 
+  apply Eqdep_dec.eq_proofs_unicity; auto; intros.
+  repeat decide equality.
+  congruence.
+Qed.
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index f837de422..8fa680a72 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -1,4 +1,4 @@
-Require Import Qfield.
+Require Import Qfield Qreduction.
 
 Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1.
 Proof.
@@ -201,4 +201,33 @@ setoid_replace (a^2) with ((-a)*(-a)) by ring.
 rewrite Qle_minus_iff in A.
 setoid_replace (0+ - a) with (-a) in A by ring.
 apply Qmult_le_0_compat; assumption.
-Qed.
\ No newline at end of file
+Qed.
+
+Theorem Qpower_decomp: forall p x y,
+  Qpower_positive (x #y) p == x ^ Zpos p # (Z2P ((Zpos y) ^ Zpos p)).
+Proof.
+induction p; intros; unfold Qmult; simpl.
+(* xI *)
+rewrite IHp, xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
+repeat rewrite Zpower_pos_is_exp.
+red; unfold Qmult, Qnum, Qden, Zpower.
+repeat rewrite Zpos_mult_morphism.
+repeat rewrite Z2P_correct.
+repeat rewrite Zpower_pos_1_r; ring.
+apply Zpower_pos_pos; red; auto.
+repeat apply Zmult_lt_0_compat; auto;
+ apply Zpower_pos_pos; red; auto.
+(* xO *)
+rewrite IHp, <-Pplus_diag.
+repeat rewrite Zpower_pos_is_exp.
+red; unfold Qmult, Qnum, Qden, Zpower.
+repeat rewrite Zpos_mult_morphism.
+repeat rewrite Z2P_correct; try ring.
+apply Zpower_pos_pos; red; auto.
+repeat apply Zmult_lt_0_compat; auto;
+ apply Zpower_pos_pos; red; auto.
+(* xO *)
+unfold Qmult; simpl.
+red; simpl; rewrite Zpower_pos_1_r;
+ rewrite Zpos_mult_morphism; ring.
+Qed.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index ddd9b0a26..6b16cfff4 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -177,3 +177,17 @@ Add Morphism Qminus' : Qminus'_comp.
   intros; unfold Qminus' in |- *.
   rewrite H; rewrite H0; auto with qarith.
 Qed.
+
+Lemma Qred_opp: forall q, Qred (-q) = - (Qred q).
+Proof.
+  intros (x, y); unfold Qred; simpl.
+  rewrite Zggcd_opp; case Zggcd; intros p1 (p2, p3); simpl.
+  unfold Qopp; auto.
+Qed.
+
+Theorem Qred_compare: forall x y,
+  Qcompare x y = Qcompare (Qred x) (Qred y).
+Proof.
+  intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct.
+Qed.
+