proposition: Lemma Qpower_minus: forall (a : Q) (n m : Z), ~ a == 0 -> a ^ (n - m) == a ^ n / a ^ m.
proof: Proof. intros a n m Hnz. rewrite <- Z.add_opp_r. rewrite Qpower_plus by assumption. rewrite Qpower_opp. field. apply Qpower_not_0; assumption. Qed.
imports: Zpow_facts Qfield Qreduction