proposition: Lemma Qpower_positive_zero : forall p, Qpower_positive 0 p == 0%Q.
proof: Proof. induction p ; simpl; try rewrite IHp ; reflexivity. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant