proposition: Lemma cc_IR_nexp : forall (x : IR) (n : nat), cc_IR x[^]n [=] cc_IR (x[^]n).
proof: Proof. intros. induction n as [| n Hrecn]; intros. astepl ([1]:CC). Step_final (cc_IR [1]). astepl (cc_IR x[^]n[*]cc_IR x). astepl (cc_IR (x[^]n) [*]cc_IR x). Step_final (cc_IR (x[^]n[*]x)). Qed.
imports: CoRN.reals.NRootIR