---

Step * of Lemma mon_nat_op_add

∀[g:IMonoid]. ∀[e:|g|]. ∀[a,b:ℕ].  (((a + b) ⋅ e) = ((a ⋅ e) * (b ⋅ e)) ∈ |g|)
BY
{ ProveSpecializedLemma `nat_op_add` 0 [parm{i}] (FoldC `mon_nat_op`) }

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[e:|g|].  \mforall{}[a,b:\mBbbN{}].    (((a  +  b)  \mcdot{}  e)  =  ((a  \mcdot{}  e)  *  (b  \mcdot{}  e)))


By

---

Latex:
ProveSpecializedLemma  `nat\_op\_add`  0  [parm\{i\}]  (FoldC  `mon\_nat\_op`)

---

Home Index