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 **)
let nat_of_bool = function
| Bool.True -> Nat.S Nat.O
| Bool.False -> Nat.O