Step * of Lemma le_weakening

a,b:ℤ.  a ≤ supposing b ∈ ℤ
BY
((UnivCD THENA Auto) THEN (RWO "le-iff-less-or-equal" THENA Auto)) }

1
1. : ℤ@i
2. : ℤ@i
3. b ∈ ℤ
⊢ a < b ∨ (a b ∈ ℤ)


Latex:


Latex:
\mforall{}a,b:\mBbbZ{}.    a  \mleq{}  b  supposing  a  =  b


By


Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "le-iff-less-or-equal"  0  THENA  Auto))




Home Index