---

Step * of Lemma bm_cnt_prop_pos

∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  0 ≤ bm_numItems(m) supposing ↑bm_cnt_prop(m)
BY
{ (Auto
   THEN (FLemma `bm_count_prop` [-1] THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN BLemma `bm_count_prop_pos`
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[m:binary\_map(T;Key)].    0  \mleq{}  bm\_numItems(m)  supposing  \muparrow{}bm\_cnt\_prop(m)


By

(Auto
  THEN  (FLemma  `bm\_count\_prop`  [-1]  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  BLemma  `bm\_count\_prop\_pos`
  THEN  Auto)

---

Home Index