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