proposition: Lemma pow_inject_Q : forall {R : ConstructiveReals} (q : Q) (n : nat), ~(q == 0)%Q -> (CR_of_Q R (q ^ Z.of_nat n) == CRpow (CR_of_Q R q) n).
proof: Proof. induction n. - intros. reflexivity. - intros. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Qpower_plus. rewrite CR_of_Q_mult, IHn. simpl. apply CRmult_comm. exact H. exact H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal