proposition: Lemma Ceq_minus (c c' : C) : c = c' <-> c-c' = 0.
proof: Proof. split; intros H. - subst c. apply Cplus_opp_r. - destruct c as (x,y), c' as (x',y'). compute in H. injection H as Hx Hy. apply Rminus_diag_uniq_sym in Hx. apply Rminus_diag_uniq_sym in Hy. now f_equal. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy