Step
*
1
1
of Lemma
mon_nat_op_one
1. g : IMonoid
2. e : |g|
⊢ (((1 - 1) ⋅ e) * e) = e ∈ |g|
BY
{ % Too tedious! Should fix zero lemma to not
require 0 constant %
((RW IntNormC 0 THENM RWH (LemmaC `mon_nat_op_zero`) 0) THENA Auto) }
1
1. g : IMonoid
2. e : |g|
⊢ (e * e) = e ∈ |g|
Latex:
Latex:
1. g : IMonoid
2. e : |g|
\mvdash{} (((1 - 1) \mcdot{} e) * e) = e
By
Latex:
\% Too tedious! Should fix zero lemma to not
require 0 constant \%
((RW IntNormC 0 THENM RWH (LemmaC `mon\_nat\_op\_zero`) 0) THENA Auto)
Home
Index