proposition: Theorem in_progression: forall n a i, In i (progression n a) <-> a <= i < n + a.
proof: Proof. intros n; elim n; simpl; auto. intros a i; split; try (intros H; case H; fail); intros (H1, H2); contradict H1; auto with arith. intros n1 Rec a i; case (Rec (S a) i); clear Rec; intros H1 H2. split; intros H. case H; intros H3; subst; auto with arith. case H1; try rewrite plus_n_Sm; auto with arith. case H; intros H3 H4. case le_lt_eq_dec with (1 := H3); auto with arith. rewrite plus_n_Sm in H4; auto with arith. Qed.
imports: List ListAux UList OrderedList