proposition: Lemma CRpow_proper : forall {R : ConstructiveReals} (x y : CRcarrier R) (n : nat), x == y -> CRpow x n == CRpow y n.
proof: Proof. induction n. - intros. reflexivity. - intros. simpl. rewrite IHn, H. + reflexivity. + exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum