---

Step * of Lemma mon_nat_op_unroll

∀[g:IMonoid]. ∀[n:ℕ+]. ∀[e:|g|].  ((n ⋅ e) = (((n - 1) ⋅ e) * e) ∈ |g|)
BY
{ UnivCD 
THENM RepUnfolds ``nat_op mon_nat_op`` 0 
THENA Auto }

1
1. g : IMonoid
2. n : ℕ+
3. e : |g|
⊢ Π(*,e) 0 ≤ i < n. e = (Π(*,e) 0 ≤ i < n - 1. e * e) ∈ |g|

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[e:|g|].    ((n  \mcdot{}  e)  =  (((n  -  1)  \mcdot{}  e)  *  e))


By

---

Latex:
UnivCD 
THENM  RepUnfolds  ``nat\_op  mon\_nat\_op``  0 
THENA  Auto

---

Home Index