proposition: Theorem Zprogression_le_end: forall n m p, In p (progression Z.succ n m) -> (p < n + Z_of_nat m).
proof: Proof. intros n m; generalize n; elim m; clear n m; auto. intros; contradiction. intros m H n p H1; simpl in H1 |-; case H1; clear H1; intros H1. lia. apply Z.lt_le_trans with (Z.succ n + Z_of_nat m). apply H; assumption. lia. Qed.
imports: Iterator ZArith Lia UList