---

Step * of Lemma bm_compare_greater_greater_false

∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (0 < compare k1 k2 ⇒ 0 < compare k2 k1 ⇒ False)
BY
{ (Auto
   THEN Unfold `bm_compare` 2
   THEN DVarSets
   THEN Unfold `anti_sym` 4
   THEN (InstHyp [⌈k1⌉;⌈k2⌉] 4⋅ THENA Auto)
   THEN Unfold `refl` 6
   THEN InstHyp [⌈k1⌉] 6⋅
   THEN Auto
   THEN RevHypSubst' (-2) (-3)
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  Unfold  `bm\_compare`  2
  THEN  DVarSets
  THEN  Unfold  `anti\_sym`  4
  THEN  (InstHyp  [\mkleeneopen{}k1\mkleeneclose{};\mkleeneopen{}k2\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  Unfold  `refl`  6
  THEN  InstHyp  [\mkleeneopen{}k1\mkleeneclose{}]  6\mcdot{}
  THEN  Auto
  THEN  RevHypSubst'  (-2)  (-3)
  THEN  Auto)

---

Home Index