open Preamble

open Div_and_mod

open Jmeq

open Russell

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Util

open Exp

open Setoids

open Monad

open Option

open Extranat

open Vector

open FoldStuff

open BitVector

open Arithmetic

val nat_of_bool : Bool.bool -> Nat.nat