---

Step * of Lemma bm_compare_trans_le

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

---

Latex:


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


By

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

---

Home Index