@user21820 So I was trying to prove this theorem for the construction of ℤ.

☐ ∀p,q,p',q'∈ℕ×ℕ ( p ~ p' ∧ q ~ q' ⇒ p+q ~ p'+q' ).

I think I succeeded in finding a proof.

Proof:
Given p,q,p',q' ∈ ℕ×ℕ
	If	p ~ p' ∧ q ~ q':
		Let p = (a1,b1)
		Let p'= (c1,d1)
		Let q = (a2,b2)
		Let q' = (c2,d2)

		a1+d1 = b1+c1
		a2+d2 = b2+c2

		p+q = (a1+a2,b1+b2)
		p'+q' = (c1+c2,d1+d2)

		a1+a2+d1+d2 = a1+d1+a2+d2 = b1+c1+b2+c2 = b1+b2+c1+c2
		p+q ~ p'+q'

But then I tried to prove this.

☐ ∀p,q,p',q'∈ℕ×ℕ ( p ~ p' ∧ q ~ q' ⇒ p·q ~ p'·q' ).

Unfortunately I failed to find a proof for this one.

Here is my failed attempt.

Proof:
Given p,q,p',q' ∈ ℕ×ℕ
	If	p ~ p' ∧ q ~ q':
		Let p = (a1,b1)
		Let p'= (c1,d1)
		Let q = (a2,b2)
		Let q' = (c2,d2)

		a1+d1 = b1+c1
		a2+d2 = b2+c2

		p.q = (a1.a2+b1.b2,a1.b2+b1.a2)
		p'.q' = (c1.c2+d1.d2,c1.d2+d1.c2)

		(a1+d1)(a2+d2) = (b1+c1)(b2+c2)
		a1.a2 + a1.d2 + a2.d1 + d1.d2 = b1.b2 + b1.c2 + b2.c1 + c1.c2

		(a1+d1)(b2+c2) = (b1+c1)(a2+d2)
		a1.b2 + a1.c2 + b2.d1 + c2.d1 = a2.b1 + b1.d2 + a2.c1 + c1.d2

		So,
		a1.a2 + a1.d2 + a2.d1 + d1.d2 + a1.b2 + a1.c2 + b2.d1 + c2.d1
		= a1.a2 + c2.d1 + a1.d2 + a2.d1 + d1.d2 + a1.b2 + a1.c2 + b2.d1

@PrithuBiswas To succeed, you should cut down the complexity by proving ∀p,q,r∈ℕ×ℕ ( p ~ q ⇒ p·r ~ q·r ), and then using this twice with commutativity to get what you want. Commutativity is easy, right?