proposition: Lemma Cinv_r (r : C) : r <> 0 -> r * /r = 1.
proof: Proof. move => H. apply injective_projections ; simpl ; field. contradict H. apply Rplus_sqr_eq_0 in H. apply injective_projections ; simpl ; by apply H. contradict H. apply Rplus_sqr_eq_0 in H. apply injective_projections ; simpl ; by apply H. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy