proposition: Theorem ulist_Zprogression: forall a n, ulist (progression Z.succ a n).
proof: Proof. intros a n; generalize a; elim n; clear a n; simpl; auto with zarith. intros n H1 a; apply ulist_cons; auto. intros H2; absurd (Z.succ a <= a); auto with zarith. apply Zprogression_le_init with ( 1 := H2 ). Qed.
imports: Iterator ZArith Lia UList