```module MiniLibrary.Real where

open import MiniLibrary.Base
open import MiniLibrary.Nat
open import MiniLibrary.Natplus
-- open import MiniLibrary.DivMod
open import MiniLibrary.Integer
open import MiniLibrary.Rational

infix 4 _<ℝ_ _≤ℝ_ _==ℝ_ _≥ℝ_
infixl 6 _+ℝ_
infixl 7 _*ℝ_

postulate ℝ     : Set
postulate _==ℝ_ : ℝ → ℝ → Set
postulate _<ℝ_  : ℝ → ℝ → Set
postulate _≤ℝ_  : ℝ → ℝ → Set
postulate _#_  : ℝ → ℝ → Set
postulate 0ℝ    : ℝ
postulate 1ℝ    : ℝ
postulate _+ℝ_  : ℝ  → ℝ  → ℝ
postulate _*ℝ_  : ℝ  → ℝ  → ℝ
postulate _-ℝ_  : ℝ  → ℝ  → ℝ
postulate recip : (r : ℝ) → r # 0ℝ → ℝ
postulate ||_|| : ℝ  → ℝ
postulate 2↑- : ℕ  → ℝ    {- 2↑- n = 2^{ -n } -}

postulate reflℝ  : (r : ℝ) → r ==ℝ r

_≥ℝ_ : ℝ → ℝ → Set
r ≥ℝ s = s ≤ℝ r

neg : ℝ → ℝ
neg r = 0ℝ  -ℝ r

divℝ : (r s : ℝ) → s # 0ℝ → ℝ
divℝ  r s p = r *ℝ (recip s p)

ℕ2ℝ : ℕ → ℝ
ℕ2ℝ  zero     = 0ℝ
ℕ2ℝ  (suc n) = ℕ2ℝ n +ℝ 1ℝ

ℕ+2ℝ : ℕ+ → ℝ
ℕ+2ℝ (suc n)  = ℕ2ℝ  n +ℝ 1ℝ

postulate ℕ+#0 : (n : ℕ+) → ℕ+2ℝ n # 0ℝ

ℤ2ℝ : ℤ → ℝ
ℤ2ℝ (+ n) = ℕ+2ℝ n
ℤ2ℝ zero = 0ℝ
ℤ2ℝ (- n) = neg (ℕ+2ℝ n)

Rat2ℝ : Rat → ℝ
Rat2ℝ (z / n) = divℝ (ℤ2ℝ z) (ℕ+2ℝ n) (ℕ+#0 n)

2ℝ  : ℝ
2ℝ  = 1ℝ +ℝ 1ℝ

3ℝ  : ℝ
3ℝ  = 2ℝ +ℝ 1ℝ

4ℝ  : ℝ
4ℝ  = 2ℝ +ℝ 2ℝ

-1ℝ  : ℝ
-1ℝ  = neg 1ℝ

postulate 2ℝ#0 : 2ℝ # 0ℝ
postulate 3ℝ#0 : 3ℝ # 0ℝ
postulate 4ℝ#0 : 4ℝ # 0ℝ

1/2ℝ  : ℝ
1/2ℝ  = divℝ 1ℝ  2ℝ 2ℝ#0

1/4ℝ  : ℝ
1/4ℝ  = divℝ 1ℝ  4ℝ 4ℝ#0

-1/2ℝ  : ℝ
-1/2ℝ  = divℝ -1ℝ  2ℝ 2ℝ#0

-1/4ℝ  : ℝ
-1/4ℝ  = divℝ -1ℝ  4ℝ 4ℝ#0

postulate _∈[-1,1]ℝ : ℝ → Set

postulate ∈[-1,1]ℝintro : (r : ℝ) → r ≥ℝ  -1ℝ → r ≤ℝ   1ℝ  → r ∈[-1,1]ℝ
postulate ∈[-1,1]ℝelim1 : (r : ℝ) → r ∈[-1,1]ℝ → r ≥ℝ  -1ℝ
postulate ∈[-1,1]ℝelim2 : (r : ℝ) → r ∈[-1,1]ℝ → r ≤ℝ  1ℝ

postulate ∈[-1,1]Rat2ℝ : (q : Rat) → q ∈[-1,1]Rat → Rat2ℝ q ∈[-1,1]ℝ
```