proposition: Lemma cc_recip_char : forall (z : CC) z_ z__, cc_recip z z_ [=] (CC_conj z[/] cc_IR (AbsCC z[^]2) [//]z__).
proof: Proof. intros z z_ HAbsCCz. unfold cc_recip in |- *. astepl (Re z[+I*][--] (Im z) [/] _[//] cc_IR_resp_ap _ _ (cc_inv_aid _ _ (cc_ap_zero _ z_))). 2: simpl in |- *; split; simpl in |- *; rational. apply div_wd with (F := CC) (x := Re z[+I*][--] (Im z)) (y := cc_IR (Re z[^]2[+]Im z[^]2)) (x' := CC_conj z) (y' := cc_IR (AbsCC z[^]2)). elim z. intros x y. simpl in |- *. split; simpl in |- *; algebra. apply cc_IR_wd. apply AbsCC_square_Re_Im with (x := Re z) (y := Im z). Qed.
imports: CoRN.complex.CComplex