proposition: Lemma CRpower_slow_wd : forall (x y : CR) (n : nat), msp_eq x y -> msp_eq (CRpower_slow x n) (CRpower_slow y n).
proof: Proof. induction n. - intros. reflexivity. - intros. simpl (CRpower_slow x (S n)). rewrite (IHn H). rewrite H. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.ProductMetric CoRN.reals.fast.CRArith Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax MathClasses.interfaces.canonical_names MathClasses.interfaces.additional_operations