namespace http://mathhub.info/MitM/core/numbertheory ❚

import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/core/typedsets ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚

theory NatIntervals : base:?Logic =
    include ☞arith:?NaturalArithmetics ❙
    include ☞sets:?TypedSets ❙

	natInterval : ℕ ⟶ ℕ ⟶ set ℕ ❘ = [a,b] ⟪ fullset ℕ | ([x] a ≤ x ∧ x ≤ b ) ⟫ ❙
❚