Lemma iterop_seq_mon_homot {n} (x y : stn n → M) : x ~ y → iterop_seq_mon(n,,x) = iterop_seq_mon(n,,y). Proof. revert x y. induction n as [|n N]. - reflexivity. - intros x y h. rewrite 2 iterop_seq_mon_step. apply two_arg_paths. + apply N. apply funhomot. exact h. + apply h. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.