apply Iff.intro
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p) ↔ ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0
case mp
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p) → ∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0

case mpr
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
⊢ (∃ a, ∃ g, p ≈ [(a, g)] ∧ a ≠ 0) → trivialNonZeroElem (Quotient.mk (formalSumSetoid R G) p)