---

Step * of Lemma qmax-assoc

∀[x,y,z:ℚ].  (qmax(qmax(x;y);z) = qmax(x;qmax(y;z)) ∈ ℚ)
BY
{ xxx(Auto
      THEN Unfold `qmax` 0
      THEN AutoBoolCase ⌜q_le(x;y)⌝⋅
      THEN AutoBoolCase ⌜q_le(y;z)⌝⋅
      THEN AutoBoolCase ⌜q_le(x;z)⌝⋅
      THEN AutoBoolCase ⌜q_le(x;y)⌝⋅
      THEN ∀h:hyp. (RWO "qle_complement_qorder" h THENA Auto) 
      THEN RelRST
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbQ{}].    (qmax(qmax(x;y);z)  =  qmax(x;qmax(y;z)))


By

---

Latex:
xxx(Auto
        THEN  Unfold  `qmax`  0
        THEN  AutoBoolCase  \mkleeneopen{}q\_le(x;y)\mkleeneclose{}\mcdot{}
        THEN  AutoBoolCase  \mkleeneopen{}q\_le(y;z)\mkleeneclose{}\mcdot{}
        THEN  AutoBoolCase  \mkleeneopen{}q\_le(x;z)\mkleeneclose{}\mcdot{}
        THEN  AutoBoolCase  \mkleeneopen{}q\_le(x;y)\mkleeneclose{}\mcdot{}
        THEN  \mforall{}h:hyp.  (RWO  "qle\_complement\_qorder"  h  THENA  Auto) 
        THEN  RelRST
        THEN  Auto)xxx

---

Home Index