proposition: Lemma cc_IR_nring : forall n : nat, cc_IR (nring n) [=] nring n.
proof: Proof. intros. induction n as [| n Hrecn]; intros. astepl (cc_IR [0]). Step_final ([0]:CC). astepl (cc_IR (nring n[+][1])). astepl (cc_IR (nring n) [+]cc_IR [1]). Step_final (nring n[+] ([1]:CC)). Qed.
imports: CoRN.reals.NRootIR