---

Step * of Lemma bm_compare_less_to_greater_eq

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

---

Latex:


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


By

(Auto
  THEN  Unfold  `bm\_compare`  2
  THEN  DVarSets
  THEN  SupposeNot
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Unfold  `connex`  5
  THEN  (InstHyp  [\mkleeneopen{}k1\mkleeneclose{};\mkleeneopen{}k2\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index