proposition: Theorem iter_le: forall (f g: Z -> Z) l, (forall a, In a l -> f a <= g a) -> iter 0 f Zplus l <= iter 0 g Zplus l.
proof: Proof. intros f g l; elim l; simpl; auto with zarith. Qed.
imports: Arith ArithRing ListAux ZArith Lia Iterator ZProgression