proposition: Lemma CRpow_plus_distr : forall {R : ConstructiveReals} (x : CRcarrier R) (n p:nat), CRpow x n * CRpow x p == CRpow x (n+p).
proof: Proof. induction n. - intros. simpl. rewrite CRmult_1_l. reflexivity. - intros. simpl. rewrite CRmult_assoc. apply CRmult_morph. + reflexivity. + apply IHn. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum