proposition: Lemma calculate_Re : forall c : CC, cc_IR (Re c) [*]Two [=] c[+]CC_conj c.
proof: Proof. intros. elim c. intros x y. intros. simpl in |- *. unfold cc_eq in |- *. simpl in |- *. split; rational. Qed.
imports: CoRN.reals.NRootIR