---

Step * of Lemma le-add-cancel4

∀[c,t,t':ℤ].  uiff((c + t) ≤ t';c ≤ 0) supposing t = t' ∈ ℤ
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `le-add-cancel3` [⌜c⌝;⌜0⌝;⌜t⌝;⌜t'⌝]⋅ THENA Auto)
   THEN Subst' 0 + t' ~ t' -1
   THEN Try (Hypothesis)) }

1
.....equality..... 
1. c : ℤ
2. t : ℤ
3. t' : ℤ
4. t = t' ∈ ℤ
5. uiff((c + t) ≤ (0 + t');c ≤ 0)
⊢ 0 + t' ~ t'

---

Latex:

---

Latex:
\mforall{}[c,t,t':\mBbbZ{}].    uiff((c  +  t)  \mleq{}  t';c  \mleq{}  0)  supposing  t  =  t'


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `le-add-cancel3`  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}t'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Subst'  0  +  t'  \msim{}  t'  -1
  THEN  Try  (Hypothesis))

---

Home Index