proposition: Lemma Qpos_power_pos : forall (x:Qpos) z, 0 < x^z.
proof: Proof. intros x z. destruct (Qle_lt_or_eq _ _ (Qpower_pos x z (Qlt_le_weak _ _ (Qpos_prf x))));[assumption|]. destruct z. discriminate H. elim (Qpower_not_0_positive x p). apply Qpos_nonzero. symmetry; assumption. elim (Qpower_not_0_positive (/x) p). change (~(Qpos_inv x) == 0). apply Qpos_nonzero. change ((/x)^p==0). rewrite -> Qinv_power. symmetry; assumption. Qed.
imports: Coq.QArith.QArith Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 Coq.Logic.Eqdep_dec CoRN.tactics.CornTac Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.Q