proposition: Lemma Qpower_positive : forall (q : Q) (n : nat), Qlt 0 q -> Qlt 0 (q^Z.of_nat n).
proof: Proof. induction n. - intros. reflexivity. - intros. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Qpower_plus. rewrite <- (Qmult_0_l q). apply Qmult_lt_r. exact H. exact (IHn H). intro abs. rewrite abs in H. inversion H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal