proposition: Lemma Qpower_not_0_positive : forall a n, ~a==0 -> ~Qpower_positive a n == 0.
proof: Proof. intros a n X H. apply X; clear X. induction n; simpl in *; try assumption; destruct (Qmult_integral _ _ H); try destruct (Qmult_integral _ _ H0); auto. Qed.
imports: Zpow_facts Qfield Qreduction