---

Step * of Lemma bag-size-bound

∀[T:Type]. ∀[as,bs:bag(T)]. ∀[n:ℕ].  #(as + bs) - n < #(bs) supposing #(as) < n
BY
{ (Auto THEN (RWO "bag-size-append" 0 THENA Auto) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].  \mforall{}[n:\mBbbN{}].    \#(as  +  bs)  -  n  <  \#(bs)  supposing  \#(as)  <  n


By

---

Latex:
(Auto  THEN  (RWO  "bag-size-append"  0  THENA  Auto)  THEN  Auto')

---

Home Index