|
|
|---|
|
|
|
|---|
Rewrite:
Some proofs of linear equalities don't work when presented as equalities because they need to be proved by linear arithmetic, but linear arithmetic only works at the literal level. This lemma allows you to state the equality as an equality rewrite rule, but breaks the equality into literals for the proof.
Theorem:
(defthm rewrite-linear-equalities-to-iff (equal (equal (< w x) (< y z)) (iff (< w x) (< y z))))