proposition: Lemma Qpower_inc : forall (n : nat) (a b : Q), 0 < a -> a <= b -> a ^ Z.of_nat n <= b ^ Z.of_nat n.
proof: Proof. induction n. - intros. discriminate. - intros. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. rewrite Qpower_plus, Qpower_plus. apply (Qle_trans _ (a * b ^ Z.of_nat n)). apply Qmult_le_l. exact H. apply IHn. exact H. exact H0. apply Qmult_le_compat_r. exact H0. apply Qpower_pos. refine (Qle_trans _ _ _ _ H0). apply Qlt_le_weak, H. intro abs. rewrite abs in H0. apply (Qlt_irrefl 0). exact (Qlt_le_trans _ _ _ H H0). intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround