proposition: Lemma Qpower_not_0: forall (a : Q) (z : Z), ~ a == 0 -> ~ Qpower a z == 0.
proof: Proof. intros a z H; destruct z. - discriminate. - apply Qpower_not_0_positive; assumption. - cbn. intros H1. pose proof Qmult_inv_r (Qpower_positive a p) as H2. specialize (H2 (Qpower_not_0_positive _ _ H)). rewrite H1, Qmult_0_r in H2. discriminate H2. Qed.
imports: Zpow_facts Qfield Qreduction