proposition: Lemma Qpower_decomp_positive p x y : Qpower_positive (x#y) p = x ^ Zpos p # (y ^ p).
proof: Proof. induction p; intros; simpl Qpower_positive; rewrite ?IHp. - unfold Qmult, Qnum, Qden. f_equal. + now rewrite <- Z.pow_twice_r, <- Z.pow_succ_r. + apply Pos2Z.inj; rewrite !Pos2Z.inj_mul, !Pos2Z.inj_pow. now rewrite <- Z.pow_twice_r, <- Z.pow_succ_r. - unfold Qmult, Qnum, Qden. f_equal. + now rewrite <- Z.pow_twice_r. + apply Pos2Z.inj; rewrite !Pos2Z.inj_mul, !Pos2Z.inj_pow. now rewrite <- Z.pow_twice_r. - now rewrite Z.pow_1_r, Pos.pow_1_r. Qed.
imports: Zpow_facts Qfield Qreduction