---

Step * 1 of Lemma has-value-monotonic


1. a : Base
2. b : Base
3. 0 ≤ eval a; 0
4. a ≤ b
⊢ 0 ≤ eval b; 0
BY
{ (Using [`b',eval a = a in 0] (BLemma `sqle_trans`)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Base
2.  b  :  Base
3.  0  \mleq{}  eval  a;  0
4.  a  \mleq{}  b
\mvdash{}  0  \mleq{}  eval  b;  0


By

---

Latex:
(Using  [`b',eval  a  =  a  in  0]  (BLemma  `sqle\_trans`)\mcdot{}  THEN  Auto)

---

Home Index