Qpower.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Zpow_facts Qfield Qreduction.

Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1.forall n : positive, Qpower_positive 1 n == 1
Proof.forall n : positive, Qpower_positive 1 n == 1
induction n;
simpl; try rewrite IHn; reflexivity.
Qed.

Lemma Qpower_1 : forall n, 1^n == 1.forall n : Z, 1 ^ n == 1
Proof.forall n : Z, 1 ^ n == 1
  intros [|n|n]; simpl; try rewrite Qpower_positive_1; reflexivity.
Qed.

Lemma Qpower_positive_0 : forall n, Qpower_positive 0 n == 0.forall n : positive, Qpower_positive 0 n == 0
Proof.forall n : positive, Qpower_positive 0 n == 0
induction n;
simpl; try rewrite IHn; reflexivity.
Qed.

Lemma Qpower_0 : forall n, (n<>0)%Z -> 0^n == 0.forall n : Z, n <> 0%Z -> 0 ^ n == 0
Proof.forall n : Z, n <> 0%Z -> 0 ^ n == 0
  intros [|n|n] Hn; try (elim Hn; reflexivity); simpl;
  rewrite Qpower_positive_0; reflexivity.
Qed.

Lemma Qpower_not_0_positive : forall a n, ~a==0 -> ~Qpower_positive a n == 0.forall (a : Q) (n : positive),
~ a == 0 -> ~ Qpower_positive a n == 0
Proof.forall (a : Q) (n : positive),
~ a == 0 -> ~ Qpower_positive a n == 0
intros a n X H.a:Q
n:positive
X:~ a == 0
H:Qpower_positive a n == 0
False
apply X; clear X.a:Q
n:positive
H:Qpower_positive a n == 0
a == 0
induction n; simpl in *; try assumption;
destruct (Qmult_integral _ _ H);
try destruct (Qmult_integral _ _ H0); auto.
Qed.

Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n.forall (p : Q) (n : positive),
0 <= p -> 0 <= Qpower_positive p n
Proof.forall (p : Q) (n : positive),
0 <= p -> 0 <= Qpower_positive p n
intros p n Hp.p:Q
n:positive
Hp:0 <= p
0 <= Qpower_positive p n
induction n; simpl; repeat apply Qmult_le_0_compat;assumption.
Qed.

Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n.forall (p : Q) (n : Z), 0 <= p -> 0 <= p ^ n
Proof.forall (p : Q) (n : Z), 0 <= p -> 0 <= p ^ n
  intros p [|n|n] Hp; simpl; try discriminate;
  try apply Qinv_le_0_compat;  apply Qpower_pos_positive; assumption.
Qed.

Lemma Qmult_power_positive  : forall a b n, Qpower_positive (a*b) n == (Qpower_positive a n)*(Qpower_positive b n).forall (a b : Q) (n : positive),
Qpower_positive (a * b) n ==
Qpower_positive a n * Qpower_positive b n
Proof.forall (a b : Q) (n : positive),
Qpower_positive (a * b) n ==
Qpower_positive a n * Qpower_positive b n
induction n;
simpl; repeat rewrite IHn; ring.
Qed.

Lemma Qmult_power : forall a b n, (a*b)^n == a^n*b^n.forall (a b : Q) (n : Z), (a * b) ^ n == a ^ n * b ^ n
Proof.forall (a b : Q) (n : Z), (a * b) ^ n == a ^ n * b ^ n
  intros a b [|n|n]; simpl;
  try rewrite Qmult_power_positive;
  try rewrite Qinv_mult_distr;
  reflexivity.
Qed.

Lemma Qinv_power_positive  : forall a n, Qpower_positive (/a) n == /(Qpower_positive a n).forall (a : Q) (n : positive),
Qpower_positive (/ a) n == / Qpower_positive a n
Proof.forall (a : Q) (n : positive),
Qpower_positive (/ a) n == / Qpower_positive a n
induction n;
simpl; repeat (rewrite IHn || rewrite Qinv_mult_distr); reflexivity.
Qed.

Lemma Qinv_power : forall a n, (/a)^n == /a^n.forall (a : Q) (n : Z), (/ a) ^ n == / a ^ n
Proof.forall (a : Q) (n : Z), (/ a) ^ n == / a ^ n
  intros a [|n|n]; simpl;
  try rewrite Qinv_power_positive;
  reflexivity.
Qed.

Lemma Qdiv_power : forall a b n, (a/b)^n == (a^n/b^n).forall (a b : Q) (n : Z), (a / b) ^ n == a ^ n / b ^ n
Proof.forall (a b : Q) (n : Z), (a / b) ^ n == a ^ n / b ^ n
unfold Qdiv.forall (a b : Q) (n : Z),
(a * / b) ^ n == a ^ n * / b ^ n
intros a b n.a, b:Q
n:Z
(a * / b) ^ n == a ^ n * / b ^ n
rewrite Qmult_power.a, b:Q
n:Z
a ^ n * (/ b) ^ n == a ^ n * / b ^ n
rewrite Qinv_power.a, b:Q
n:Z
a ^ n * / b ^ n == a ^ n * / b ^ n
reflexivity.
Qed.

Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z (Zpos p))^n.forall (n : Z) (p : positive),
(1 # p) ^ n == / inject_Z (Z.pos p) ^ n
Proof.forall (n : Z) (p : positive),
(1 # p) ^ n == / inject_Z (Z.pos p) ^ n
intros n p.n:Z
p:positive
(1 # p) ^ n == / inject_Z (Z.pos p) ^ n
rewrite Qmake_Qdiv.n:Z
p:positive
(inject_Z 1 / inject_Z (Z.pos p)) ^ n ==
/ inject_Z (Z.pos p) ^ n
rewrite Qdiv_power.n:Z
p:positive
inject_Z 1 ^ n / inject_Z (Z.pos p) ^ n ==
/ inject_Z (Z.pos p) ^ n
rewrite Qpower_1.n:Z
p:positive
1 / inject_Z (Z.pos p) ^ n == / inject_Z (Z.pos p) ^ n
unfold Qdiv.n:Z
p:positive
1 * / inject_Z (Z.pos p) ^ n ==
/ inject_Z (Z.pos p) ^ n
ring.
Qed.

Lemma Qpower_plus_positive : forall a n m, Qpower_positive a (n+m) == (Qpower_positive a n)*(Qpower_positive a m).forall (a : Q) (n m : positive),
Qpower_positive a (n + m) ==
Qpower_positive a n * Qpower_positive a m
Proof.forall (a : Q) (n m : positive),
Qpower_positive a (n + m) ==
Qpower_positive a n * Qpower_positive a m
intros a n m.a:Q
n, m:positive
Qpower_positive a (n + m) ==
Qpower_positive a n * Qpower_positive a m
unfold Qpower_positive.a:Q
n, m:positive
pow_pos Qmult a (n + m) ==
pow_pos Qmult a n * pow_pos Qmult a m
apply pow_pos_add.a:Q
n, m:positive
Equivalence (fun q q0 : Q => q == q0)
a:Q
n, m:positive
Proper
  ((fun q q0 : Q => q == q0) ==>
   (fun q q0 : Q => q == q0) ==>
   (fun q q0 : Q => q == q0)) Qmult
a:Q
n, m:positive
forall x y z : Q, x * (y * z) == x * y * z
apply Q_Setoid.a:Q
n, m:positive
Proper
  ((fun q q0 : Q => q == q0) ==>
   (fun q q0 : Q => q == q0) ==>
   (fun q q0 : Q => q == q0)) Qmult
a:Q
n, m:positive
forall x y z : Q, x * (y * z) == x * y * z
apply Qmult_comp.a:Q
n, m:positive
forall x y z : Q, x * (y * z) == x * y * z
apply Qmult_assoc.
Qed.

Lemma Qpower_opp : forall a n, a^(-n) == /a^n.forall (a : Q) (n : Z), a ^ (- n) == / a ^ n
Proof.forall (a : Q) (n : Z), a ^ (- n) == / a ^ n
intros a [|n|n]; simpl; try reflexivity.a:Q
n:positive
Qpower_positive a n == / / Qpower_positive a n
symmetry; apply Qinv_involutive.
Qed.

Lemma Qpower_minus_positive : forall a (n m:positive),
  (m < n)%positive ->
  Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m).forall (a : Q) (n m : positive),
(m < n)%positive ->
Qpower_positive a (n - m) ==
Qpower_positive a n / Qpower_positive a m
Proof.forall (a : Q) (n m : positive),
(m < n)%positive ->
Qpower_positive a (n - m) ==
Qpower_positive a n / Qpower_positive a m
intros a n m H.a:Q
n, m:positive
H:(m < n)%positive
Qpower_positive a (n - m) ==
Qpower_positive a n / Qpower_positive a m
destruct (Qeq_dec a 0) as [EQ|NEQ].a:Q
n, m:positive
H:(m < n)%positive
EQ:a == 0
Qpower_positive a (n - m) ==
Qpower_positive a n / Qpower_positive a m
a:Q
n, m:positive
H:(m < n)%positive
NEQ:~ a == 0
Qpower_positive a (n - m) ==
Qpower_positive a n / Qpower_positive a m
-a:Q
n, m:positive
H:(m < n)%positive
EQ:a == 0
Qpower_positive a (n - m) ==
Qpower_positive a n / Qpower_positive a m now rewrite EQ, !Qpower_positive_0.
-a:Q
n, m:positive
H:(m < n)%positive
NEQ:~ a == 0
Qpower_positive a (n - m) ==
Qpower_positive a n / Qpower_positive a m rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by
   (now apply Qpower_not_0_positive).a:Q
n, m:positive
H:(m < n)%positive
NEQ:~ a == 0
Qpower_positive a (n - m) * Qpower_positive a m /
Qpower_positive a m ==
Qpower_positive a n / Qpower_positive a m
  f_equiv.a:Q
n, m:positive
H:(m < n)%positive
NEQ:~ a == 0
Qpower_positive a (n - m) * Qpower_positive a m ==
Qpower_positive a n
  rewrite <- Qpower_plus_positive.a:Q
n, m:positive
H:(m < n)%positive
NEQ:~ a == 0
Qpower_positive a (n - m + m) == Qpower_positive a n
  now rewrite Pos.sub_add.
Qed.

Lemma Qpower_plus : forall a n m, ~a==0 -> a^(n+m) == a^n*a^m.forall (a : Q) (n m : Z),
~ a == 0 -> a ^ (n + m) == a ^ n * a ^ m
Proof.forall (a : Q) (n m : Z),
~ a == 0 -> a ^ (n + m) == a ^ n * a ^ m
intros a [|n|n] [|m|m] H; simpl; try ring;
try rewrite Qpower_plus_positive;
try apply Qinv_mult_distr; try reflexivity;
rewrite ?Z.pos_sub_spec;
case Pos.compare_spec; intros H0; simpl; subst;
 try rewrite Qpower_minus_positive;
 try (field; try split; apply Qpower_not_0_positive);
 assumption.
Qed.

Lemma Qpower_plus' : forall a n m, (n+m <> 0)%Z -> a^(n+m) == a^n*a^m.forall (a : Q) (n m : Z),
(n + m)%Z <> 0%Z -> a ^ (n + m) == a ^ n * a ^ m
Proof.forall (a : Q) (n m : Z),
(n + m)%Z <> 0%Z -> a ^ (n + m) == a ^ n * a ^ m
intros a n m H.a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
a ^ (n + m) == a ^ n * a ^ m
destruct (Qeq_dec a 0)as [X|X].a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
X:a == 0
a ^ (n + m) == a ^ n * a ^ m
a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
X:~ a == 0
a ^ (n + m) == a ^ n * a ^ m
rewrite X.a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
X:a == 0
0 ^ (n + m) == 0 ^ n * 0 ^ m
a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
X:~ a == 0
a ^ (n + m) == a ^ n * a ^ m
rewrite Qpower_0 by assumption.a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
X:a == 0
0 == 0 ^ n * 0 ^ m
a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
X:~ a == 0
a ^ (n + m) == a ^ n * a ^ m
destruct n; destruct m; try (elim H; reflexivity);
 simpl; repeat rewrite Qpower_positive_0; ring_simplify;
 reflexivity.a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
X:~ a == 0
a ^ (n + m) == a ^ n * a ^ m
apply Qpower_plus.a:Q
n, m:Z
H:(n + m)%Z <> 0%Z
X:~ a == 0
~ a == 0
assumption.
Qed.

Lemma Qpower_mult_positive : forall a n m,
  Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m.forall (a : Q) (n m : positive),
Qpower_positive a (n * m) ==
Qpower_positive (Qpower_positive a n) m
Proof.forall (a : Q) (n m : positive),
Qpower_positive a (n * m) ==
Qpower_positive (Qpower_positive a n) m
intros a n m.a:Q
n, m:positive
Qpower_positive a (n * m) ==
Qpower_positive (Qpower_positive a n) m
induction n using Pos.peano_ind.a:Q
m:positive
Qpower_positive a (1 * m) ==
Qpower_positive (Qpower_positive a 1) m
a:Q
n, m:positive
IHn:Qpower_positive a (n * m) == Qpower_positive (Qpower_positive a n) m
Qpower_positive a (Pos.succ n * m) ==
Qpower_positive (Qpower_positive a (Pos.succ n)) m
 reflexivity.a:Q
n, m:positive
IHn:Qpower_positive a (n * m) == Qpower_positive (Qpower_positive a n) m
Qpower_positive a (Pos.succ n * m) ==
Qpower_positive (Qpower_positive a (Pos.succ n)) m
rewrite Pos.mul_succ_l.a:Q
n, m:positive
IHn:Qpower_positive a (n * m) == Qpower_positive (Qpower_positive a n) m
Qpower_positive a (m + n * m) ==
Qpower_positive (Qpower_positive a (Pos.succ n)) m
rewrite <- Pos.add_1_l.a:Q
n, m:positive
IHn:Qpower_positive a (n * m) == Qpower_positive (Qpower_positive a n) m
Qpower_positive a (m + n * m) ==
Qpower_positive (Qpower_positive a (1 + n)) m
do 2 rewrite Qpower_plus_positive.a:Q
n, m:positive
IHn:Qpower_positive a (n * m) == Qpower_positive (Qpower_positive a n) m
Qpower_positive a m * Qpower_positive a (n * m) ==
Qpower_positive
  (Qpower_positive a 1 * Qpower_positive a n) m
rewrite IHn.a:Q
n, m:positive
IHn:Qpower_positive a (n * m) == Qpower_positive (Qpower_positive a n) m
Qpower_positive a m *
Qpower_positive (Qpower_positive a n) m ==
Qpower_positive
  (Qpower_positive a 1 * Qpower_positive a n) m
rewrite Qmult_power_positive.a:Q
n, m:positive
IHn:Qpower_positive a (n * m) == Qpower_positive (Qpower_positive a n) m
Qpower_positive a m *
Qpower_positive (Qpower_positive a n) m ==
Qpower_positive (Qpower_positive a 1) m *
Qpower_positive (Qpower_positive a n) m
reflexivity.
Qed.

Lemma Qpower_mult : forall a n m, a^(n*m) ==  (a^n)^m.forall (a : Q) (n m : Z), a ^ (n * m) == (a ^ n) ^ m
Proof.forall (a : Q) (n m : Z), a ^ (n * m) == (a ^ n) ^ m
intros a [|n|n] [|m|m]; simpl;
 try rewrite Qpower_positive_1;
 try rewrite Qpower_mult_positive;
 try rewrite Qinv_power_positive;
 try rewrite Qinv_involutive;
 try reflexivity.
Qed.

Lemma Zpower_Qpower : forall (a n:Z), (0<=n)%Z -> inject_Z (a^n) == (inject_Z a)^n.forall a n : Z,
(0 <= n)%Z -> inject_Z (a ^ n) == inject_Z a ^ n
Proof.forall a n : Z,
(0 <= n)%Z -> inject_Z (a ^ n) == inject_Z a ^ n
intros a [|n|n] H;[reflexivity| |elim H; reflexivity].a:Z
n:positive
H:(0 <= Z.pos n)%Z
inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
induction n using Pos.peano_ind.a:Z
H:(0 <= 1)%Z
inject_Z (a ^ 1) == inject_Z a ^ 1
a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.pos (Pos.succ n)) ==
inject_Z a ^ Z.pos (Pos.succ n)
 replace (a^1)%Z with a by ring.a:Z
H:(0 <= 1)%Z
inject_Z a == inject_Z a ^ 1
a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.pos (Pos.succ n)) ==
inject_Z a ^ Z.pos (Pos.succ n)
 ring.a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.pos (Pos.succ n)) ==
inject_Z a ^ Z.pos (Pos.succ n)
rewrite Pos2Z.inj_succ.a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.succ (Z.pos n)) ==
inject_Z a ^ Z.succ (Z.pos n)
unfold Z.succ.a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ (Z.pos n + 1)) ==
inject_Z a ^ (Z.pos n + 1)
rewrite Zpower_exp; auto with *; try discriminate.a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.pos n * a ^ 1) ==
inject_Z a ^ (Z.pos n + 1)
rewrite Qpower_plus' by discriminate.a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.pos n * a ^ 1) ==
inject_Z a ^ Z.pos n * inject_Z a ^ 1
rewrite <- IHn by discriminate.a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.pos n * a ^ 1) ==
inject_Z (a ^ Z.pos n) * inject_Z a ^ 1
replace (a^Zpos n*a^1)%Z with (a^Zpos n*a)%Z by ring.a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.pos n * a) ==
inject_Z (a ^ Z.pos n) * inject_Z a ^ 1
ring_simplify.a:Z
n:positive
H:(0 <= Z.pos (Pos.succ n))%Z
IHn:(0 <= Z.pos n)%Z -> inject_Z (a ^ Z.pos n) == inject_Z a ^ Z.pos n
inject_Z (a ^ Z.pos n * a) ==
inject_Z (a ^ Z.pos n) * inject_Z a
reflexivity.
Qed.

Lemma Qsqr_nonneg : forall a, 0 <= a^2.forall a : Q, 0 <= a ^ 2
Proof.forall a : Q, 0 <= a ^ 2
intros a.a:Q
0 <= a ^ 2
destruct (Qlt_le_dec 0 a) as [A|A].a:Q
A:0 < a
0 <= a ^ 2
a:Q
A:a <= 0
0 <= a ^ 2
apply (Qmult_le_0_compat a a);
 (apply Qlt_le_weak; assumption).a:Q
A:a <= 0
0 <= a ^ 2
setoid_replace (a^2) with ((-a)*(-a)) by ring.a:Q
A:a <= 0
0 <= - a * - a
rewrite Qle_minus_iff in A.a:Q
A:0 <= 0 + - a
0 <= - a * - a
setoid_replace (0+ - a) with (-a) in A by ring.a:Q
A:0 <= - a
0 <= - a * - a
apply Qmult_le_0_compat; assumption.
Qed.

Theorem Qpower_decomp p x y :
  Qpower_positive (x#y) p = x ^ Zpos p # (y ^ p).p:positive
x:Z
y:positive
Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
Proof.p:positive
x:Z
y:positive
Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
induction p; intros; simpl Qpower_positive; rewrite ?IHp.p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(x # y) *
((x ^ Z.pos p # y ^ p) * (x ^ Z.pos p # y ^ p)) =
x ^ Z.pos p~1 # y ^ p~1
p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(x ^ Z.pos p # y ^ p) * (x ^ Z.pos p # y ^ p) =
x ^ Z.pos p~0 # y ^ p~0
x:Z
y:positive
x # y = x ^ 1 # y ^ 1
- (* xI *)p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(x # y) *
((x ^ Z.pos p # y ^ p) * (x ^ Z.pos p # y ^ p)) =
x ^ Z.pos p~1 # y ^ p~1
  unfold Qmult, Qnum, Qden.p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
x * (x ^ Z.pos p * x ^ Z.pos p) # y * (y ^ p * y ^ p) =
x ^ Z.pos p~1 # y ^ p~1 f_equal.p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(x * (x ^ Z.pos p * x ^ Z.pos p))%Z =
(x ^ Z.pos p~1)%Z
p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(y * (y ^ p * y ^ p))%positive = (y ^ p~1)%positive
  +p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(x * (x ^ Z.pos p * x ^ Z.pos p))%Z =
(x ^ Z.pos p~1)%Z now rewrite <- Z.pow_twice_r, <- Z.pow_succ_r.
  +p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(y * (y ^ p * y ^ p))%positive = (y ^ p~1)%positive apply Pos2Z.inj; rewrite !Pos2Z.inj_mul, !Pos2Z.inj_pow.p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(Z.pos y * (Z.pos y ^ Z.pos p * Z.pos y ^ Z.pos p))%Z =
(Z.pos y ^ Z.pos p~1)%Z
    now rewrite <- Z.pow_twice_r, <- Z.pow_succ_r.
- (* xO *)p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(x ^ Z.pos p # y ^ p) * (x ^ Z.pos p # y ^ p) =
x ^ Z.pos p~0 # y ^ p~0
  unfold Qmult, Qnum, Qden.p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
x ^ Z.pos p * x ^ Z.pos p # y ^ p * y ^ p =
x ^ Z.pos p~0 # y ^ p~0 f_equal.p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(x ^ Z.pos p * x ^ Z.pos p)%Z = (x ^ Z.pos p~0)%Z
p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(y ^ p * y ^ p)%positive = (y ^ p~0)%positive
  +p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(x ^ Z.pos p * x ^ Z.pos p)%Z = (x ^ Z.pos p~0)%Z now rewrite <- Z.pow_twice_r.
  +p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(y ^ p * y ^ p)%positive = (y ^ p~0)%positive apply Pos2Z.inj; rewrite !Pos2Z.inj_mul, !Pos2Z.inj_pow.p:positive
x:Z
y:positive
IHp:Qpower_positive (x # y) p = x ^ Z.pos p # y ^ p
(Z.pos y ^ Z.pos p * Z.pos y ^ Z.pos p)%Z =
(Z.pos y ^ Z.pos p~0)%Z
    now rewrite <- Z.pow_twice_r.
- (* xO *)x:Z
y:positive
x # y = x ^ 1 # y ^ 1
  now rewrite Z.pow_1_r, Pos.pow_1_r.
Qed.