proposition: Theorem next_n_Z: forall n m, next_n Z.succ n m = n + Z_of_nat m.
proof: Proof. intros n m; generalize n; elim m; clear n m. intros n; simpl; auto with zarith. intros m H n. replace (n + Z_of_nat (S m)) with (Z.succ n + Z_of_nat m). rewrite <- H; auto with zarith. rewrite inj_S; auto with zarith. Qed.
imports: Iterator ZArith Lia UList