proposition: Lemma Cminus_eq_contra : forall r1 r2 : C, r1 <> r2 -> r1 - r2 <> 0.
proof: Proof. intros ; contradict H ; apply injective_projections ; apply Rminus_diag_uniq. now apply (f_equal (@fst R R)) in H. now apply (f_equal (@snd R R)) in H. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy