proposition: Lemma Zeqb_Ccomplete z z' : RtoC (IZR z) = RtoC (IZR z') -> Z.eqb z z' = true.
proof: Proof. intros H. apply Z.eqb_eq. now apply eq_IZR, RtoC_inj. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy