proposition: Lemma CRpow_gt_zero : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat), 0 < x -> 0 < CRpow x n.
proof: Proof. induction n. - intros. apply CRzero_lt_one. - intros. simpl. apply CRmult_lt_0_compat. + exact H. + apply IHn. exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum