proposition: Lemma CRpow_ge_one : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat), 1 <= x -> 1 <= CRpow x n.
proof: Proof. induction n. - intros. apply CRle_refl. - intros. simpl. apply (CRle_trans _ (x * 1)). + rewrite CRmult_1_r. exact H. + apply CRmult_le_compat_l_half. * apply (CRlt_le_trans _ 1). -- apply CRzero_lt_one. -- exact H. * apply IHn. exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum