proposition: Lemma Qpower0 : forall z, (z <> 0)%Z -> (0 ^ z == 0)%Q.
proof: Proof. unfold Qpower. destruct z;intros. - congruence. - apply Qpower_positive_zero. - rewrite Qpower_positive_zero. reflexivity. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant