proposition: Theorem progression_S_le_init: forall n m p, In p (progression S n m) -> le n p.
proof: Proof. intros n m; generalize n; elim m; clear n m; simpl; auto. intros; contradiction. intros m H n p [H1|H1]; auto with arith. subst n; auto. apply le_S_n; auto with arith. Qed.
imports: List Permutation Arith