Library Coqtail.mytheories.myReals.MyNNR

Require Import Reals Rpow_facts.
Local Open Scope R_scope.

Definition nnr_sqr (r : R) : nonnegreal.
Proof.
∃ (r ^ 2) ; apply pow2_pos.
Defined.

Definition nnr_abs (r : R) : nonnegreal.
Proof.
∃ (Rabs r) ; apply Rabs_pos.
Defined.