---

Step * of Lemma grp_op_preserves_le_qorder

No Annotations
∀[x,y,z:ℚ].  (x + y) ≤ (x + z) supposing y ≤ z
BY
{ ((ProveSpecializedLemmaWReduce grp_op_preserves_le) 0 [⌜parm{i}⌝;⌜<ℚ+>⌝]⋅ THEN Fold `qle` (-1) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y,z:\mBbbQ{}].    (x  +  y)  \mleq{}  (x  +  z)  supposing  y  \mleq{}  z


By

---

Latex:
((ProveSpecializedLemmaWReduce  grp\_op\_preserves\_le)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}
  THEN  Fold  `qle`  (-1)
  THEN  Auto)

---

Home Index