proposition: Lemma CRpow_mult : forall {R : ConstructiveReals} (x y : CRcarrier R) (n:nat), CRpow x n * CRpow y n == CRpow (x*y) n.
proof: Proof. induction n. - simpl. rewrite CRmult_1_r. reflexivity. - simpl. rewrite <- IHn. do 2 rewrite <- (Rmul_assoc (CRisRing R)). apply CRmult_morph. + reflexivity. + rewrite <- (Rmul_comm (CRisRing R)). rewrite <- (Rmul_assoc (CRisRing R)). apply CRmult_morph. * reflexivity. * rewrite <- (Rmul_comm (CRisRing R)). reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum