proposition: Theorem in_Zprogression: forall a b n, ( a <= b < a + Z_of_nat n ) -> In b (progression Z.succ a n).
proof: Proof. intros a b n; generalize a b; elim n; clear a b n; auto with zarith. simpl; auto with zarith. intros n H a b. replace (a + Z_of_nat (S n)) with (Z.succ a + Z_of_nat n). intros [H1 H2]; simpl; auto with zarith. case (Zle_lt_or_eq _ _ H1); auto with zarith. rewrite inj_S; auto with zarith. Qed.
imports: Iterator ZArith Lia UList