proposition: Lemma Qpower_positive_abs_le : forall (q:Q) (c : Qpos) (n : positive), Qabs q <= `c -> Qabs (Qpower_positive q n) <= Qpower_positive (` c) n.
proof: Proof. intros q c. induction n. - intros. simpl (Qpower_positive q n~1). rewrite Qabs_Qmult. simpl (Qpower_positive (` c) n~1). apply (Qle_trans _ (`c * Qabs (Qpower_positive q n * Qpower_positive q n))). apply Qmult_le_compat_r. exact H. apply Qabs_nonneg. apply Qmult_le_l. apply Qpos_ispos. rewrite Qabs_Qmult. apply (Qle_trans _ (Qpower_positive (`c) n * Qabs (Qpower_positive q n))). apply Qmult_le_compat_r. apply IHn. exact H. apply Qabs_nonneg. rewrite Qmult_comm. apply Qmult_le_compat_r. apply IHn. exact H. apply Qpower_pos_positive, Qpos_nonneg. - intros. simpl (Qpower_positive q n~0). rewrite Qabs_Qmult. simpl. apply (Qle_trans _ (Qpower_positive (`c) n * Qabs (Qpower_positive q n))). apply Qmult_le_compat_r. apply IHn. exact H. apply Qabs_nonneg. rewrite Qmult_comm. apply Qmult_le_compat_r. apply IHn. exact H. apply Qpower_pos_positive, Qpos_nonneg. - intros. exact H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.ProductMetric CoRN.reals.fast.CRArith Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax MathClasses.interfaces.canonical_names MathClasses.interfaces.additional_operations