---

Step * of Lemma bm_compare_greater_to_less_eq

∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (0 < compare k1 k2 ⇒ ((compare k2 k1) ≤ 0))
BY
{ (Auto
   THEN Unfold `bm_compare` 2
   THEN DVarSets
   THEN SupposeNot
   THEN Assert ⌈False⌉⋅
   THEN Auto
   THEN (Assert ⌈0 < compare k2 k1⌉⋅ THENA Auto)
   THEN FLemma `bm_compare_greater_greater_false` [-3;-1]
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  Unfold  `bm\_compare`  2
  THEN  DVarSets
  THEN  SupposeNot
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}0  <  compare  k2  k1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  FLemma  `bm\_compare\_greater\_greater\_false`  [-3;-1]
  THEN  Auto)

---

Home Index