---

Step * 1 of Lemma bm_compare_connex_le


1. K : Type
2. compare : K ─→ K ─→ ℤ@i
3. Trans(K;x,y.0 ≤ (compare x y))@i
4. AntiSym(K;x,y.0 ≤ (compare x y))@i
5. Connex(K;x,y.0 ≤ (compare x y))@i
6. Refl(K;x,y.(compare x y) = 0 ∈ ℤ)@i
7. Sym(K;x,y.(compare x y) = 0 ∈ ℤ)@i
8. k1 : K@i
9. k2 : K@i
10. ¬(0 ≤ (compare k1 k2))
⊢ 0 ≤ (compare k2 k1)
BY
{ Assert ⌈(0 ≤ (compare k2 k1)) ∨ (0 ≤ (compare k1 k2))⌉⋅ }

1
.....assertion..... 
1. K : Type
2. compare : K ─→ K ─→ ℤ@i
3. Trans(K;x,y.0 ≤ (compare x y))@i
4. AntiSym(K;x,y.0 ≤ (compare x y))@i
5. Connex(K;x,y.0 ≤ (compare x y))@i
6. Refl(K;x,y.(compare x y) = 0 ∈ ℤ)@i
7. Sym(K;x,y.(compare x y) = 0 ∈ ℤ)@i
8. k1 : K@i
9. k2 : K@i
10. ¬(0 ≤ (compare k1 k2))
⊢ (0 ≤ (compare k2 k1)) ∨ (0 ≤ (compare k1 k2))

2
1. K : Type
2. compare : K ─→ K ─→ ℤ@i
3. Trans(K;x,y.0 ≤ (compare x y))@i
4. AntiSym(K;x,y.0 ≤ (compare x y))@i
5. Connex(K;x,y.0 ≤ (compare x y))@i
6. Refl(K;x,y.(compare x y) = 0 ∈ ℤ)@i
7. Sym(K;x,y.(compare x y) = 0 ∈ ℤ)@i
8. k1 : K@i
9. k2 : K@i
10. ¬(0 ≤ (compare k1 k2))
11. (0 ≤ (compare k2 k1)) ∨ (0 ≤ (compare k1 k2))
⊢ 0 ≤ (compare k2 k1)

---

Latex:



1.  K  :  Type
2.  compare  :  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbZ{}@i
3.  Trans(K;x,y.0  \mleq{}  (compare  x  y))@i
4.  AntiSym(K;x,y.0  \mleq{}  (compare  x  y))@i
5.  Connex(K;x,y.0  \mleq{}  (compare  x  y))@i
6.  Refl(K;x,y.(compare  x  y)  =  0)@i
7.  Sym(K;x,y.(compare  x  y)  =  0)@i
8.  k1  :  K@i
9.  k2  :  K@i
10.  \mneg{}(0  \mleq{}  (compare  k1  k2))
\mvdash{}  0  \mleq{}  (compare  k2  k1)


By

Assert  \mkleeneopen{}(0  \mleq{}  (compare  k2  k1))  \mvee{}  (0  \mleq{}  (compare  k1  k2))\mkleeneclose{}\mcdot{}

---

Home Index