---

Step * of Lemma decidable__rat-cube-face-ext

∀k:ℕ. ∀c,d:ℚCube(k).  Dec(c ≤ d)
BY
{ Extract of Obid: decidable__rat-cube-face
  not unfolding  q_le qless qeq int_seg_decide
  finishing with (Fold `rat-cube-face-decider` 0 THEN Auto)
  normalizes to:
  
  λk,c,d. rat-cube-face-decider(k;c;d) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c,d:\mBbbQ{}Cube(k).    Dec(c  \mleq{}  d)


By

---

Latex:
Extract  of  Obid:  decidable\_\_rat-cube-face
not  unfolding    q\_le  qless  qeq  int\_seg\_decide
finishing  with  (Fold  `rat-cube-face-decider`  0  THEN  Auto)
normalizes  to:

\mlambda{}k,c,d.  rat-cube-face-decider(k;c;d)

---

Home Index