open Preamble

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

open Div_and_mod

val exp : Nat.nat -> Nat.nat -> Nat.nat