Lemmas useful to prove some of the theorems about set-size.
The lemma
Theorem:
(defthm len-when-no-duplicatesp-and-subsetp (implies (and (no-duplicatesp-equal x) (subsetp-equal x y)) (<= (len x) (len y))))
Theorem:
(defthm len-when-no-duplicatesp-and-strict-subsetp (implies (and (no-duplicatesp-equal x) (subsetp-equal x y) (not (subsetp-equal y x))) (< (len x) (len y))))