Step
*
of Lemma
mon_nat_op_wf
∀[g:IMonoid]. ∀[n:ℕ]. ∀[e:|g|].  (n ⋅ e ∈ |g|)
BY
{ Unfold `mon_nat_op` 0 THEN Auto }
Latex:
Latex:
\mforall{}[g:IMonoid].  \mforall{}[n:\mBbbN{}].  \mforall{}[e:|g|].    (n  \mcdot{}  e  \mmember{}  |g|)
By
Latex:
Unfold  `mon\_nat\_op`  0  THEN  Auto
Home
Index