Lemma iterop_list_mon_singleton (x : M) : iterop_list_mon (x::[]) = x. Proof. reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.