proposition: Lemma Cmod_mult : forall x y, Cmod (x * y) = (Cmod x * Cmod y)%R.
proof: Proof. intros x y. unfold Cmod. rewrite -sqrt_mult. apply f_equal ; simpl ; ring. apply Rplus_le_le_0_compat ; apply pow2_ge_0. apply Rplus_le_le_0_compat ; apply pow2_ge_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy