proposition: Lemma Qinv_power_positive : forall a n, Qpower_positive (/a) n == /(Qpower_positive a n).
proof: Proof. induction n; simpl; repeat (rewrite IHn || rewrite Qinv_mult_distr); reflexivity. Qed.
imports: Zpow_facts Qfield Qreduction