English
For every natural number n, if you take unpair n to be (a,b), then pairing a and b yields n: pair a b = n.
Русский
Для каждого натурального числа n, если unpair n = (a,b), то pair a b = n.
LaTeX
$$$ \forall n \in \mathbb{N}, \; \operatorname{pair}(\operatorname{fst}(\operatorname{unpair}(n)), \operatorname{snd}(\operatorname{unpair}(n))) = n. $$$
Lean4
@[simp]
theorem pair_unpair (n : ℕ) : pair (unpair n).1 (unpair n).2 = n :=
by
dsimp only [unpair]; let s := sqrt n
have sm : s * s + (n - s * s) = n := Nat.add_sub_cancel' (sqrt_le _)
split_ifs with h
· simp [s, pair, h, sm]
· have hl : n - s * s - s ≤ s :=
Nat.sub_le_iff_le_add.2 (Nat.sub_le_iff_le_add'.2 <| by rw [← Nat.add_assoc]; apply sqrt_le_add)
simp [s, pair, hl.not_gt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]
