proposition: Lemma nexp_power : forall p : nat, nexp IR p Two[=]nring (power p 2).
proof: Proof. simple induction p. simpl in |- *. algebra. intros n H. astepr (nring (R:=IR) (power n 2 * 2)). astepr (nring (R:=IR) (power n 2)[*]Two). astepl (nexp IR n Two[*]Two). apply mult_wdl. exact H. Qed.
imports: CoRN.metrics.CPseudoMSpaces