Section AbsCC_properties.
Lemma AbsCC_nonneg : forall x : C, 0 [<=] AbsCC x.
Lemma AbsCC_ap_zero_imp_pos : forall z : C, AbsCC z [#] 0 -> 0 [<] AbsCC z.
Lemma AbsCC_wd : forall x y : C, x [=] y -> AbsCC x [=] AbsCC y.
Lemma cc_inv_abs : forall x : C, AbsCC [--]x [=] AbsCC x.
Lemma cc_minus_abs : forall x y : C, AbsCC (x[-]y) [=] AbsCC (y[-]x).
Lemma cc_mult_abs : forall x y : C, AbsCC (x[*]y) [=] AbsCC x[*]AbsCC y.
Lemma AbsCC_minzero : forall x : C, AbsCC (x[-]0) [=] AbsCC x.
Lemma AbsCC_IR : forall x : IR, 0 [<=] x -> AbsCC (cc_IR x) [=] x.
Lemma cc_div_abs : forall (x y : C) y_ y__, AbsCC (x[/] y[//]y_) [=] (AbsCC x[/] AbsCC y[//]y__).
Lemma cc_div_abs' : forall (x : C) (y : IR) y_ y__,
0 [<=] y -> AbsCC (x[/] cc_IR y[//]y__) [=] (AbsCC x[/] y[//]y_).
Lemma AbsCC_zero : AbsCC 0 [=] 0.
Lemma AbsCC_one : AbsCC 1 [=] 1.
Lemma cc_pow_abs : forall (x : C) (n : N), AbsCC (x[^]n) [=] AbsCC x[^]n.
Lemma AbsCC_pos : forall x : C, x [#] 0 -> 0 [<] AbsCC x.
Lemma AbsCC_ap_zero : forall x : C, 0 [#] AbsCC x -> x [#] 0.
Lemma AbsCC_small_imp_eq : forall x : C, (forall e, 0 [<] e -> AbsCC x [<] e) -> x [=] 0.
Lemma AbsCC_square_Re_Im : forall x y : IR, x[^]2[+]y[^]2 [=] AbsCC (x[+I*]y) [^]2.
Lemma AbsCC_mult_conj : forall z : C, z[*]CC_conj z [=] cc_IR (AbsCC z[^]2).
Lemma AbsCC_mult_square : forall x y : C, AbsCC (x[*]y) [^]2 [=] AbsCC x[^]2[*]AbsCC y[^]2.
Lemma AbsCC_square_ap_zero : forall z : C, z [#] 0 -> AbsCC z[^]2 [#] 0.
Lemma cc_recip_char : forall (z : C) z_ z__,
cc_recip z z_ [=] (CC_conj z[/] cc_IR (AbsCC z[^]2) [//]z__).
Lemma AbsCC_strext : fun_strext AbsCC.
Definition AbsSmallCC (e : IR) (x : C) := AbsCC x [<=] e.
Lemma Cexis_AFS_CC : forall x y ε, 0 [<] ε -> {y' : C | AbsSmallCC ε (y'[-]y) | y' [#] x}.
End AbsCC_properties.