proposition: Lemma CRpow_inv : forall {R : ConstructiveReals} (x : CRcarrier R) (xPos : 0 < x) (n : nat), CRpow (CRinv R x (inr xPos)) n == CRinv R (CRpow x n) (inr (CRpow_gt_zero x n xPos)).
proof: Proof. induction n. - rewrite CRinv_1. reflexivity. - transitivity (CRinv R x (inr xPos) * CRpow (CRinv R x (inr xPos)) n). + reflexivity. + rewrite IHn. assert (0 < x * CRpow x n). { apply CRmult_lt_0_compat. * exact xPos. * apply CRpow_gt_zero, xPos. } rewrite <- (CRinv_mult_distr _ _ _ _ (inr H)). apply CRinv_morph. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum