proposition: Lemma AbsCC_small_imp_eq : forall x : CC, (forall e, [0] [<] e -> AbsCC x [<] e) -> x [=] [0].
proof: Proof. intros x H. apply not_ap_imp_eq. intro. elim (less_irreflexive_unfolded _ (AbsCC x)). apply H. apply AbsCC_pos. auto. Qed.
imports: CoRN.complex.CComplex