proposition: Lemma calculate_Im : forall c : CC, cc_IR (Im c) [*] (Two[*]II) [=] 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