proposition: Lemma Qpos_power_ispos : forall (x:Qpos) (z : Z), 0 < proj1_sig x^z.
proof: Proof. intros x z. assert (0 < proj1_sig x) as xpos by (destruct x; exact q). destruct (Qle_lt_or_eq _ _ (Qpower_pos (proj1_sig x) z (Qlt_le_weak _ _ xpos)));[assumption|]. destruct z. discriminate H. elim (Qpower_not_0_positive (proj1_sig x) p). destruct x. intro abs. simpl in abs. clear H xpos. rewrite abs in q. exact (Qlt_irrefl 0 q). symmetry; assumption. elim (Qpower_not_0_positive (/proj1_sig x) p). change (~proj1_sig (Qpos_inv x) == 0). destruct (Qpos_inv x). intro abs. simpl in abs. clear H xpos. rewrite abs in q. exact (Qlt_irrefl 0 q). change ((/proj1_sig x)^Z.pos p==0). rewrite -> Qinv_power. symmetry; assumption. Qed.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder