Section Mult_CC_Continuous.
Lemma mult_absCC : forall (x y : C) (X Y : IR),
AbsCC x [<=] X -> AbsCC y [<=] Y -> AbsCC (x[*]y) [<=] X[*]Y.
Lemma estimate_absCC : forall x : C, {X : IR | 0 [<] X | AbsCC x [<=] X}.
Lemma mult_CC_contin : forall (x y : C) (e : IR),
0 [<] e -> {c : IR | 0 [<] c | {d : IR | 0 [<] d | forall x' y',
AbsCC (x[-]x') [<=] c -> AbsCC (y[-]y') [<=] d -> AbsCC (x[*]y[-]x'[*]y') [<=] e}}.
End Mult_CC_Continuous.
Section CPoly_CC_Continuous.
Let g be a polynomial over the complex numbers.
Variable g : C[X].
Lemma cpoly_CC_contin : forall (x : C) (e : IR), 0 [<] e ->
{d : IR | 0 [<] d | forall x', AbsCC (x[-]x') [<=] d -> AbsCC (g ! x[-]g ! x') [<=] e}.
Lemma contin_polyCC : CCcontin (fun x => g ! x).
End CPoly_CC_Continuous.