---

Step * of Lemma rotate-inverse

∀[n:ℕ+]. (inv(rot(n)) = rot(n)^n - 1 ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )
BY
{ (Auto THEN BLemma `funinv-unique` THEN Auto THEN BLemma `rotate-inverse1` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  (inv(rot(n))  =  rot(n)\^{}n  -  1)


By

---

Latex:
(Auto  THEN  BLemma  `funinv-unique`  THEN  Auto  THEN  BLemma  `rotate-inverse1`  THEN  Auto)

---

Home Index