Module infotheo.lib.coqRE

From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum.
From Coq Require Reals.
From mathcomp Require Import lra.
From mathcomp Require Import Rstruct.

Import Order.POrderTheory GRing.Theory Num.Theory.


Lemma R1E : (Rdefinitions.IZR (BinNums.Zpos BinNums.xH)) = 1%R.

Proof.

by []. Qed.

Lemma R0E : (Rdefinitions.IZR BinNums.Z0) = 0%R.

Proof.

by []. Qed.

Definition

coqRE

coqRE not a defined object.

:=
  (R0E, R1E, INRE, IZRposE,
    RinvE, RoppE, RdivE, RminusE, RplusE, RmultE, RpowE, RsqrtE).