Definition loop_power {Y} {y:Y} (l:y = y) (n:ℤ) : y = y. Proof. intros. assert (m := loop_power_nat l (hzabsval n)). destruct (hzlthorgeh n 0%hz). { exact (!m). } { exact m. } Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.