proposition: Lemma Qpower_0_lt: forall (a : Q) (z : Z), 0 < a -> 0 < Qpower a z.
proof: Proof. intros q z Hpos. pose proof Qpower_pos q z (Qlt_le_weak 0 q Hpos) as H1. pose proof Qpower_not_0 q z as H2. pose proof Qlt_not_eq 0 q Hpos as H3. specialize (H2 (Qnot_eq_sym _ _ H3)); clear H3. apply Qnot_eq_sym in H2. apply Qlt_leneq; split; assumption. Qed.
imports: Zpow_facts Qfield Qreduction