From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum matrix.
From mathcomp Require Import boolp reals classical_sets signed topology functions.
From mathcomp Require Import prodnormedzmodule normedtype landau forms derive.

Set Implicit Arguments.

Import Order.Theory.
Import GRing.Theory.
Import Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section Foo.
Context (R: realType).
Check (`[0: R, 1: R]%classic).
End Foo.