proposition: Lemma Cmod_eq_0 : forall x, Cmod x = 0 -> x = 0.
proof: Proof. intros x H. unfold Cmod, pow in H. rewrite 2!Rmult_1_r -sqrt_0 in H. apply sqrt_inj in H. apply Rplus_sqr_eq_0 in H. now apply injective_projections. apply Rplus_le_le_0_compat ; apply Rle_0_sqr. apply Rle_refl. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy