Rules about limits not being 0.
These two rules serve to relieve the recurring hypothesis
that the limit is never 0 during the symbolic execution.
Initially the limit is a variable, and the first rule applies;
the hypothesis of this rule is easily discharged by
the inequality assumption over the initial limit
in the symbolic execution theorem,
via ACL2's linear arithmetic.
The syntaxp hypothesis restricts the application of the rule
to the case in which the limit is a variable (which is true initially).
As the symbolic execution proceeds,
1 gets repeatedly subtracted from the initial limit variable,
and it appears that ACL2 automatically combines multiple 1s
into constants larger than 1,
giving the pattern
Theorem:
(defthm not-zp-of-limit-variable (implies (and (syntaxp (symbolp limit)) (integerp limit) (> limit 0)) (not (zp limit))))
Theorem:
(defthm not-zp-of-limit-minus-const (implies (and (syntaxp (quotep -c)) (integerp -c) (integerp limit) (> limit (- -c))) (not (zp (binary-+ -c limit)))))