proposition: Lemma AbsCC_ap_zero_imp_pos : forall z : CC, AbsCC z [#] [0] -> [0] [<] AbsCC z.
proof: Proof. intros z H. apply leEq_not_eq. apply AbsCC_nonneg. apply ap_symmetric_unfolded. assumption. Qed.
imports: CoRN.complex.CComplex