proposition: Theorem progression_list: forall n m, ulist (progression n m).
proof: Proof. assert (E1: forall n m p , In p (progression n m) -> m <= p). intros n; elim n; simpl; auto with datatypes; clear n. intros m p H; case H. intros n Rec m p [H | H]; subst; auto with arith. apply Nat.le_trans with (S m); auto with arith. intros n; elim n; simpl; clear n; auto. intros n Rec m; apply ulist_cons; auto. intros H; generalize (E1 _ _ _ H); auto with arith. intros H1; contradict H1; auto with arith. Qed.
imports: List ListAux UList OrderedList