proposition: Lemma pow2inv : forall {R : ConstructiveReals} (n p:nat), CRpow (CR_of_Q R 2) n * CRpow (CR_of_Q R (1 # 2)) (n + p) == CRpow (CR_of_Q R (1 # 2)) p.
proof: Proof. induction p. - simpl. rewrite Nat.add_0_r, CRpow_mult. rewrite (CRpow_proper (CR_of_Q R 2 * CR_of_Q R (1 # 2)) 1). apply CRpow_one. rewrite <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. reflexivity. reflexivity. - rewrite Nat.add_succ_r. transitivity (CRpow (CR_of_Q R 2) n * (CR_of_Q R (1 # 2) * CRpow (CR_of_Q R (1 # 2)) (n + p))). reflexivity. rewrite <- CRmult_assoc. rewrite (CRmult_comm (CRpow (CR_of_Q R 2) n)). rewrite CRmult_assoc, IHp. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions