Lemma iterop_list_mon_step (x:M) (xs:list M) : iterop_list_mon (x::xs) = x * iterop_list_mon xs. Proof. apply iterop_list_step. apply runax. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.