---

Step * 1 1 1 1 of Lemma assert_of_eq_int


1. x : ℤ
2. y : ℤ
3. ↑if x=y then tt else ff
4. (x + (-x)) = 0 ∈ ℤ
⊢ ¬x < x
BY
{ ((D 0 THENA Auto) THEN (Assert x + (-x) < x + (-x) BY (BLemma `add-monotonic` THEN Auto))) }

1
1. x : ℤ
2. y : ℤ
3. ↑if x=y then tt else ff
4. (x + (-x)) = 0 ∈ ℤ
5. x < x
6. x + (-x) < x + (-x)
⊢ False

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  \muparrow{}if  x=y  then  tt  else  ff
4.  (x  +  (-x))  =  0
\mvdash{}  \mneg{}x  <  x


By

---

Latex:
((D  0  THENA  Auto)  THEN  (Assert  x  +  (-x)  <  x  +  (-x)  BY  (BLemma  `add-monotonic`  THEN  Auto)))

---

Home Index