Theorem: LoVe.Int.add_Eq (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
p₁ n₁ p₂ n₂ : ℕ
⊢ add (Quotient.mk Setoid (p₁, n₁)) (Quotient.mk Setoid (p₂, n₂)) = Quotient.mk Setoid (p₁ + p₂, n₁ + n₂)
Tactic:
rfl
State after:
no goals