---

Step * 1 of Lemma mreducible_elim


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
⊢ ∃b,c:|g|. ((¬(g-unit(b))) ∧ (¬(g-unit(c))) ∧ (a = (b * c) ∈ |g|)) ⇐⇒ ∃b:|g|. ((¬(g-unit(b))) ∧ (b p| a))
BY
{ ((RWH (LemmaC `exists_over_and_r`) 0) THENA Auto) }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
⊢ ∃b:|g|. ((¬(g-unit(b))) ∧ (∃c:|g|. ((¬(g-unit(c))) ∧ (a = (b * c) ∈ |g|)))) ⇐⇒ ∃b:|g|. ((¬(g-unit(b))) ∧ (b p| a))

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  a  :  |g|
\mvdash{}  \mexists{}b,c:|g|.  ((\mneg{}(g-unit(b)))  \mwedge{}  (\mneg{}(g-unit(c)))  \mwedge{}  (a  =  (b  *  c)))
\mLeftarrow{}{}\mRightarrow{}  \mexists{}b:|g|.  ((\mneg{}(g-unit(b)))  \mwedge{}  (b  p|  a))


By

---

Latex:
((RWH  (LemmaC  `exists\_over\_and\_r`)  0)  THENA  Auto)

---

Home Index