---

Step * 1 of Lemma mon_nat_op_one


1. g : IMonoid
2. e : |g|
⊢ (1 ⋅ e) = e ∈ |g|
BY
{ ((RWH (LemmaC `mon_nat_op_unroll`) 0) THENA Auto) 
 }

1
1. g : IMonoid
2. e : |g|
⊢ (((1 - 1) ⋅ e) * e) = e ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  e  :  |g|
\mvdash{}  (1  \mcdot{}  e)  =  e


By

---

Latex:
((RWH  (LemmaC  `mon\_nat\_op\_unroll`)  0)  THENA  Auto) 

---

Home Index