---

Step * 1 of Lemma imax_ge_left


1. a : @i
2. b : @i
 imax(a;b)  a 
BY
{ (Decide a  b THENA Auto) }

1
1. a : @i
2. b : @i
3. a  b
 imax(a;b)  a 

2
1. a : @i
2. b : @i
3. (a  b)
 imax(a;b)  a 

---

Latex:



1.  a  :  \mBbbZ{}@i
2.  b  :  \mBbbZ{}@i
\mvdash{}  imax(a;b)  \mgeq{}  a 


By

(Decide  \mkleeneopen{}a  \mleq{}  b\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index