proposition: Lemma Qpower_minus_neg: forall (a b : positive) (n m : Z), (Z.neg a#b) ^ (n - m) == (Z.neg a#b) ^ n * (Z.neg b#a) ^ m.
proof: Proof. intros a b n m. rewrite Qpower_minus by discriminate. rewrite <- (Qinv_neg b a), Qinv_power. reflexivity. Qed.
imports: Zpow_facts Qfield Qreduction