Smaug123

-- https://math.stackexchange.com/a/4894379/259262

import Mathlib.Data.Real.Sqrt
import Mathlib.Tactic.Hint
import Mathlib.Tactic.Cases
import Mathlib.Algebra.Order.Floor

open Real Set

namespace Problem

Smaug123

module Range where

-- Preliminaries

record True : Set where
data False : Set where
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
data _||_ (A : Set) (B : Set) : Set where

Smaug123

Keybase proof

I hereby claim:

• I am smaug123 on github.
• I am patrickstevens (https://keybase.io/patrickstevens) on keybase.
• I have a public key ASAXpP1UQX-aNITZNR8uGTEIh64umJJxGQAAQcoPBIY-bQo

To claim this, I am signing this object: