Library Waterproof.Notations.RealsWithSubsets
Require Import Coq.Reals.Reals.
Require Import Notations.Common.
Require Import Notations.Sets.
Require Import Notations.Reals.
Require Import Libs.Reals.
Declare Scope R2_scope.
Notation "'ℤ'" := Z_in_R : R2_scope.
Notation "'ℚ'" := Q_in_R : R2_scope.
Open Scope R_scope.
Open Scope subset_scope.
Open Scope R2_scope.
Notation "q 'is' 'rational'" := (is_rational q) (at level 70) : R2_scope.
Notation "q 'is' 'irrational'" := (¬(q is rational)) (at level 70) : R2_scope.
Notation " A 'is' 'a' 'single' 'interval'" := (is_interval A) (at level 70) : R_scope.
Require Import Notations.Common.
Require Import Notations.Sets.
Require Import Notations.Reals.
Require Import Libs.Reals.
Declare Scope R2_scope.
Notation "'ℤ'" := Z_in_R : R2_scope.
Notation "'ℚ'" := Q_in_R : R2_scope.
Open Scope R_scope.
Open Scope subset_scope.
Open Scope R2_scope.
Notation "q 'is' 'rational'" := (is_rational q) (at level 70) : R2_scope.
Notation "q 'is' 'irrational'" := (¬(q is rational)) (at level 70) : R2_scope.
Notation " A 'is' 'a' 'single' 'interval'" := (is_interval A) (at level 70) : R_scope.