proposition: Lemma cc_ap_zero : forall P : CC -> Prop, (forall a b, a [#] [0] -> P (a[+I*]b)) -> (forall a b, b [#] [0] -> P (a[+I*]b)) -> forall c, c [#] [0] -> P c.
proof: Proof. intros ????. elim c. intros a b H1. elim H1; intros H2; auto. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing