I managed to prove it using Wikipedia's approach, using theorems from Standard Library.

```
Require Import Nat Arith Lia.
Set Implicit Arguments.
Definition Cantor_pairing x y := ((x + y + 1) * (x + y)) / 2 + y.
Definition Cantor_pairing_inv (z: nat): nat * nat.
Proof.
set ((sqrt (8 * z + 1) - 1) / 2) as w. set (div (w * w + w) 2) as t. set (z - t) as y. set (w - y) as x.
exact (x, y).
Defined.
Theorem Cantor_pairing_inv_thm z x y: Cantor_pairing x y = z -> (x, y) = Cantor_pairing_inv z.
Proof.
intros. unfold Cantor_pairing in H. remember (x + y) as w. remember ((w + 1) * w / 2) as t.
assert (2 * t = w * w + w).
{ rewrite Heqt. clear Heqt Heqw. induction w; auto.
replace ((S w + 1) * S w) with ((w + 1) * w + (w + 1) * 2) by ring.
rewrite Nat.div_add. ring_simplify. rewrite IHw. ring. lia. }
assert ((2 * w + 1) * (2 * w + 1) <= 8 * z + 1) by lia.
assert (8 * z + 1 < (2 * S w + 1) * (2 * S w + 1)) by lia.
assert (2 * w + 1 <= sqrt (8 * z + 1)).
{ apply Nat.sqrt_le_square in H1. auto. }
assert (sqrt (8 * z + 1) < 2 * S w + 1).
{ apply Nat.sqrt_lt_square in H2. auto. }
assert (2 * w <= sqrt (8 * z + 1) - 1 < 2 * S w) by lia.
assert (w <= (sqrt (8 * z + 1) - 1) / 2).
{ apply Nat.div_le_lower_bound; lia. }
assert ((sqrt (8 * z + 1) - 1) / 2 < S w).
{ apply Nat.div_lt_upper_bound; lia. }
assert (w = (sqrt (8 * z + 1) - 1) / 2) by lia.
assert (y = z - t) by lia. assert (x = w - y) by lia.
unfold Cantor_pairing_inv. rewrite <- H8, <- H0. replace (2 * t) with (t * 2) by ring.
rewrite Nat.div_mul; try lia. f_equal; lia.
Qed.
Definition injective A B (f: A -> B) := forall x y, f x = f y -> x = y.
Definition countable A := exists (f: A -> nat), injective f.
Theorem countable_mult A B: countable A -> countable B -> countable (A * B).
Proof.
intros. destruct H as [f H], H0 as [f0 H0].
exists (fun p => match p with (x, y) => Cantor_pairing (f x) (f0 y) end).
intros [x1 y1] [x2 y2] H1.
assert ((f x1, f0 y1) = Cantor_pairing_inv (Cantor_pairing (f x2) (f0 y2))).
{ apply Cantor_pairing_inv_thm. auto. }
assert ((f x2, f0 y2) = Cantor_pairing_inv (Cantor_pairing (f x2) (f0 y2))).
{ apply Cantor_pairing_inv_thm. auto. }
assert ((f x1, f0 y1) = (f x2, f0 y2)) by congruence.
inversion H4. apply H in H6. apply H0 in H7. congruence.
Qed.
```

Big thank you anyway! :)

Lessness has marked this topic as resolved.

@Lessness

Oops, I forgot to give a (maybe) useful information:

Gödel's proof mechanization (by Russel O'Connor) is maintained on Coq-community: https://github.com/coq-community/goedel

Note also a nice Gödel-like theorem, which I didn't have time to fully mechanize: "The termination of Goodstein sequences and hydra battles cannot be proven in Peano arithmetic" (see the paper by Kirby and Paris https://faculty.baruch.cuny.edu/lkirby/accessible_independence_results.pdf )

You can find results on Cantor pairing in the standard library: https://coq.inria.fr/library/Coq.Arith.Cantor.html

with some discussion and links: https://github.com/coq/coq/pull/14008

@Gert Smolka has a chapter on Cantor's pairing in his book: https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf#chapter.7

Last updated: Feb 04 2023 at 21:02 UTC