proposition: Lemma Qpower_positive_eq_zero : forall q p, Qpower_positive q p == 0 -> q == 0.
proof: Proof. unfold Qpower_positive. induction p ; simpl; intros; repeat match goal with | H : _ * _ == 0 |- _ => apply Qmult_integral in H; destruct H end; tauto. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant