proposition: Lemma powerPositive : forall {R : ConstructiveReals} (n:nat), (0 < CRpow (CR_of_Q R 2) n).
proof: Proof. intros. apply CRpow_gt_zero. simpl. apply CR_of_Q_lt. reflexivity. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits