---

Step * 1 of Lemma half-pi-interval-proper


1. i-finite((-(π/2(slower)), π/2(slower)))
⊢ -(π/2(slower)) < π/2(slower)
BY
{ (InstLemma `half-pi-positive` [] THEN DupHyp (-1) THEN nRAdd ⌜-(π/2(slower))⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  i-finite((-(\mpi{}/2(slower)),  \mpi{}/2(slower)))
\mvdash{}  -(\mpi{}/2(slower))  <  \mpi{}/2(slower)


By

---

Latex:
(InstLemma  `half-pi-positive`  []  THEN  DupHyp  (-1)  THEN  nRAdd  \mkleeneopen{}-(\mpi{}/2(slower))\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index