fact: Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x) := match z with | neg n => loopexp_pos p^ n | zero => 1 | pos n => loopexp_pos p n end.
imports: Basics Types.Universe Spaces.Pos Spaces.Int.Core Spaces.Int.Spec Spaces.Int.Equiv