---

Step * of Lemma bm_compare_less_less_false

∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (compare k1 k2 < 0 ⇒ compare k2 k1 < 0 ⇒ False)
BY
{ (Auto THEN FLemma `bm_compare_less_to_greater_eq` [-2] THEN Auto) }

---

Latex:


\mforall{}[K:Type].  \mforall{}[compare:bm\_compare(K)].  \mforall{}[k1,k2:K].    (compare  k1  k2  <  0  {}\mRightarrow{}  compare  k2  k1  <  0  {}\mRightarrow{}  False)


By

(Auto  THEN  FLemma  `bm\_compare\_less\_to\_greater\_eq`  [-2]  THEN  Auto)

---

Home Index