proposition: Lemma Cmod_R : forall x : R, Cmod x = Rabs x.
proof: Proof. intros x. unfold Cmod. simpl. rewrite Rmult_0_l Rplus_0_r Rmult_1_r. apply sqrt_Rsqr_abs. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy