FAQ

• How to use MathComp-Analysis' Boolean operators with the real numbers of the Coq standard library?

The following script provides an example but this "feature" is untested:

From Coq Require Import Reals.

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum.

From mathcomp.analysis Require Import
boolp ereal reals posnum landau classical_sets Rstruct Rbar topology prodnormedzmodule normedtype.

Local Open Scope ring_scope.

Check (0 <= 1 :> R). (* (0 : R) <= (1 : R) : bool *)