---

Step * of Lemma bm_compare_antisym_le

∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  ((0 ≤ (compare k1 k2)) ⇒ (0 ≤ (compare k2 k1)) ⇒ (k1 = k2 ∈ K))
BY
{ (Auto THEN Unfold `bm_compare` 2 THEN DVarSets THEN Auto) }

---

Latex:


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


By

(Auto  THEN  Unfold  `bm\_compare`  2  THEN  DVarSets  THEN  Auto)

---

Home Index