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