---

Step * of Lemma omon_lt_mono_imp_leq_mono

∀[g:OMon]. {∀[a:|g|]. monot(|g|;x,y.x ≤ y;λz.(a * z))} supposing ∀a:|g|. monot(|g|;x,y.x < y;λz.(a * z))
BY
{ ((Eval ``guard monot`` 0 
THEN RepD) THENA Auto) }

1
1. g : OMon
2. ∀a,x,y:|g|.  ((x < y) ⇒ ((a * x) < (a * y)))
3. a : |g|
4. x : |g|
5. y : |g|
6. x ≤ y
⊢ (a * x) ≤ (a * y)

---

Latex:

---

Latex:
\mforall{}[g:OMon]
    \{\mforall{}[a:|g|].  monot(|g|;x,y.x  \mleq{}  y;\mlambda{}z.(a  *  z))\}  supposing  \mforall{}a:|g|.  monot(|g|;x,y.x  <  y;\mlambda{}z.(a  *  z))


By

---

Latex:
((Eval  ``guard  monot``  0 
THEN  RepD)  THENA  Auto)

---

Home Index