---

Step * of Lemma exp_preserves_le

∀[n,x,y:ℕ].  x^n ≤ y^n supposing x ≤ y
BY
{ (InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN Unfold `exp` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN Fold `exp` 0) }

1
1. n : ℤ
2. n ≠ 0
3. 0 < n
4. ∀[x,y:ℕ].  x^n - 1 ≤ y^n - 1 supposing x ≤ y
5. x : ℕ
6. y : ℕ
7. x ≤ y
⊢ (x * x^n - 1) ≤ (y * y^n - 1)

---

Latex:

---

Latex:
\mforall{}[n,x,y:\mBbbN{}].    x\^{}n  \mleq{}  y\^{}n  supposing  x  \mleq{}  y


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  Unfold  `exp`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Fold  `exp`  0)

---

Home Index