Library Interval.Missing.MathComp2

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq: http://tamadi.gforge.inria.fr/CoqApprox/

This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/

As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From HB Require Import structures.
From Coq Require Import Rdefinitions Raxioms RIneq Rbasic_fun.
From mathcomp.ssreflect Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq bigop.

Set Implicit Arguments.

Definition eqr (r1 r2 : R) : bool :=
if Req_EM_T r1 r2 is left _ then true else false.

Lemma eqrP : Equality.axiom eqr.

Fact RplusA : associative (Rplus).

Fact RmultA : associative (Rmult).

Import Monoid.

Module BigOp.
Notation bigopE := bigop.unlock.
End BigOp.