proposition: Lemma CC_conj_nexp : forall (c : CC) n, CC_conj (c[^]n) [=] CC_conj c[^]n.
proof: Proof. intros. induction n as [| n Hrecn]; intros. astepl (CC_conj [1]). Step_final ([1]:CC). astepl (CC_conj (c[^]n[*]c)). astepl (CC_conj (c[^]n) [*]CC_conj c). Step_final (CC_conj c[^]n[*]CC_conj c). Qed.
imports: CoRN.reals.NRootIR