proposition: Lemma cc_div_abs : forall (x y : CC) y_ y__, AbsCC (x[/] y[//]y_) [=] (AbsCC x[/] AbsCC y[//]y__).
proof: Proof. intros x y nz anz. rstepl (AbsCC y[*]AbsCC (x[/] y[//]nz) [/] AbsCC y[//]anz). apply div_wd. 2: algebra. astepl (AbsCC (y[*] (x[/] y[//]nz))). apply AbsCC_wd. rational. Qed.
imports: CoRN.complex.CComplex