proposition: Theorem Zprogression_le_init: forall n m p, In p (progression Z.succ n m) -> (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 zarith. generalize (H _ _ H1); auto with zarith. Qed.
imports: Iterator ZArith Lia UList