---

Step * of Lemma grp_op_preserves_lt_qorder

No Annotations
∀[u,v,w:ℚ].  u + v < u + w supposing v < w
BY
{ ((ProveSpecializedLemmaWReduce grp_op_preserves_lt) 0 [⌜parm{i}⌝;⌜<ℚ+>⌝] ⋅ THEN Folds ``qless`` (-1) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[u,v,w:\mBbbQ{}].    u  +  v  <  u  +  w  supposing  v  <  w


By

---

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

---

Home Index