proposition: Lemma Qpower_decomp_pos: forall (p : positive) (a : Z) (b : positive), (a # b) ^ (Z.pos p) == a ^ (Z.pos p) # (b ^ p)%positive.
proof: Proof. intros p a b. pose proof Qpower_decomp_positive p a b. cbn; rewrite H; reflexivity. Qed.
imports: Zpow_facts Qfield Qreduction