Library Coq.micromega.ZifyPow
Require
Import
Arith
Max
Min
BinInt
BinNat
Znat
Nnat
.
Require
Import
ZifyClasses
.
Require
Export
ZifyInst
.
Instance
Op_Z_pow_pos
:
BinOp
Z.pow_pos
:=
{
TBOp
:=
Z.pow
;
TBOpInj
:=
ltac
:(
reflexivity
) }.
Add
BinOp
Op_Z_pow_pos
.