proposition: Lemma Qpower_decomp_neg_neg: forall (p a b: positive), (Z.neg a # b) ^ (Z.neg p) == (Z.neg b) ^ (Z.pos p) # (a ^ p)%positive.
proof: Proof. intros p a b. cbn. rewrite <- Qinv_power_positive, Qinv_neg. rewrite Qpower_decomp_positive. reflexivity. Qed.
imports: Zpow_facts Qfield Qreduction