proposition: Lemma Cmod_gt_0 : forall (x : C), x <> 0 <-> 0 < Cmod x.
proof: Proof. intros x ; split => Hx. destruct (Cmod_ge_0 x) => //. by apply sym_eq, Cmod_eq_0 in H. contradict Hx. apply Rle_not_lt, Req_le. by rewrite Hx Cmod_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy