Definition iterop_fun_step (lunax : islunit op unel) {m} (x:stn(S m) → X) : iterop_fun x = op (iterop_fun (x ∘ dni lastelement)) (x lastelement). Proof. intros. unfold iterop_fun at 1. simpl. induction m as [|m _]. - simpl. apply pathsinv0, lunax. - simpl. reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.