proposition: Lemma cc_div_abs' : forall (x : CC) (y : IR) y_ y__, [0] [<=] y -> AbsCC (x[/] cc_IR y[//]y__) [=] (AbsCC x[/] y[//]y_).
proof: Proof. intros x y nz cnz H. rstepl (y[*]AbsCC (x[/] cc_IR y[//]cnz) [/] y[//]nz). apply div_wd. 2: algebra. astepl (AbsCC (cc_IR y) [*]AbsCC (x[/] cc_IR y[//]cnz)). astepl (AbsCC (cc_IR y[*] (x[/] cc_IR y[//]cnz))). apply AbsCC_wd. rational. Qed.
imports: CoRN.complex.CComplex