proposition: Lemma GeoHalfBelowTwo : forall {R : ConstructiveReals} (n:nat), CRsum (CRpow (CR_of_Q R (1#2))) n < CR_of_Q R 2.
proof: Proof. intros. rewrite <- (CRplus_0_r (CR_of_Q R 2)), GeoFiniteSum. apply CRplus_lt_compat_l. rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. apply CRpow_gt_zero. apply CR_of_Q_lt. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum