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 **)
let rec exp n = function
| Nat.O -> Nat.S Nat.O
| Nat.S p -> Nat.times (exp n p) n