fact: Definition chain_correct_nat (n:nat) (c: chain) := n <> 0 /\ forall `(M:@EMonoid A E_op E_one E_eq) (x:A), chain_apply c x == x ^ n.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)