proposition: Lemma Qpower_plus_positive : forall a n m, Qpower_positive a (n+m) == (Qpower_positive a n)*(Qpower_positive a m).
proof: Proof. intros a n m. unfold Qpower_positive. apply pow_pos_add. - apply Q_Setoid. - apply Qmult_comp. - apply Qmult_assoc. Qed.
imports: Zpow_facts Qfield Qreduction