proposition: Lemma pow_nat : forall {R : ConstructiveReals} (a n : nat), CR_of_Q R (Z.of_nat (a ^ n) # 1) == CRpow (CR_of_Q R (Z.of_nat a # 1)) n.
proof: Proof. induction n. - reflexivity. - simpl. setoid_replace (Z.of_nat (a * a ^ n) # 1) with ((Z.of_nat a # 1) * (Z.of_nat (a ^ n) # 1))%Q. rewrite CR_of_Q_mult. apply CRmult_morph. reflexivity. exact IHn. rewrite Nat2Z.inj_mul. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia