---

Step * of Lemma perm_grp_inv_assoc

∀[T:Type]. ∀[a,b:Perm(T)].  ((a O inv_perm(a) O b = b ∈ Perm(T)) ∧ (inv_perm(a) O a O b = b ∈ Perm(T)))
BY
{ (ProveSpecializedLemma `grp_inv_assoc` 1 [parm{i}; perm_igrp(T)] (AbReduceC)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a,b:Perm(T)].    ((a  O  inv\_perm(a)  O  b  =  b)  \mwedge{}  (inv\_perm(a)  O  a  O  b  =  b))


By

---

Latex:
(ProveSpecializedLemma  `grp\_inv\_assoc`  1  [parm\{i\};  perm\_igrp(T)]  (AbReduceC))

---

Home Index