let neql := of_decide_eq_false neqv
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
neql : ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_false neqv
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂