proposition: Lemma Ceq_dec : forall z1 z2 : C, {z1 = z2} + {z1 <> z2}.
proof: Proof. intros z1 z2 ; destruct z1 as (r1, r2) ; destruct z2 as (r3, r4). destruct Req_or_neq with (r1- r3)%R; destruct Req_or_neq with (r2 - r4)%R. left; CusingR. right ; intro Habs ; apply Ceq in Habs ; destruct Habs ; auto with real. right ; intro Habs ; apply Ceq in Habs ; destruct Habs ; auto with real. right ; intro Habs ; apply Ceq in Habs ; destruct Habs ; auto with real. Qed.
imports: Ctacfield Cbase Cpow Lia