proposition: Lemma Ceq_dec (z1 z2 : C) : { z1 = z2 } + { z1 <> z2 }.
proof: Proof. destruct z1 as [x1 y1]. destruct z2 as [x2 y2]. case: (Req_EM_T x1 x2) => [ -> | Hx ]. case: (Req_EM_T y1 y2) => [ -> | Hy ]. by left. right ; contradict Hy. now apply (f_equal (@snd R R)) in Hy ; simpl in Hy. right ; contradict Hx. now apply (f_equal (@fst R R)) in Hx ; simpl in Hx. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy