Theory numpair

⊢ ∀n. tri⁻¹ n = SND (invtri0 n 0)

⊢ ∀n. nfst n = tri (tri⁻¹ n) + tri⁻¹ n − n

⊢ ∀m n. m ⊗ n = tri (m + n) + n

⊢ ∀n. nsnd n = n − tri (tri⁻¹ n)

⊢ tri 0 = 0 ∧ ∀n. tri (SUC n) = SUC n + tri n

⊢ ∀n a. FST (invtri0 n a) < SUC (SND (invtri0 n a))

⊢ ∀n a.
    invtri0 n a =
    if n < a + 1 then (n,a) else invtri0 (n − (a + 1)) (a + 1)

⊢ ∀P. (∀n a. (¬(n < a + 1) ⇒ P (n − (a + 1)) (a + 1)) ⇒ P n a) ⇒
      ∀v v1. P v v1

⊢ ∀n a. tri (SND (invtri0 n a)) + FST (invtri0 n a) = n + tri a

⊢ tri⁻¹ n ≤ n

⊢ tri⁻¹ (tri n) = n

⊢ y ≤ x ⇒ tri⁻¹ (tri x + y) = x

⊢ tri (tri⁻¹ n) ≤ n

⊢ tri y ≤ n ∧ n < tri (y + 1) ⇒ tri⁻¹ n = y

⊢ n < tri (tri⁻¹ n + 1)

⊢ nfst 0 = 0

⊢ nfst n ≤ n

⊢ ∀m n. n ≤ n ⊗ m

⊢ nfst (x ⊗ y) = x

⊢ ∀n. nfst n ⊗ nsnd n = n

⊢ 0 ⊗ 0 = 0

⊢ ∀n n1 n2. n ⊗ n1 < n ⊗ n2 ⇔ n1 < n2

⊢ ∀n n1 n2. n ⊗ n1 < n ⊗ n2 ⇒ n1 < n2

⊢ ∀n n1 n2. n1 < n2 ⇒ n ⊗ n1 < n ⊗ n2

⊢ x1 ⊗ y1 = x2 ⊗ y2 ⇔ x1 = x2 ∧ y1 = y2

⊢ ∀x y. x ⊗ y = 0 ⇔ x = 0 ∧ y = 0

⊢ ∀n. ∃x y. n = x ⊗ y

⊢ ∀a b c d. a ≤ b ∧ c < d ⇒ a ⊗ c < b ⊗ d

⊢ nsnd 0 = 0

⊢ nsnd n ≤ n

⊢ ∀m n. m ≤ n ⊗ m

⊢ nsnd (x ⊗ y) = y

⊢ ∀m n. tri m = tri n ⇔ m = n

⊢ ∀m n. tri m ≤ tri n ⇔ m ≤ n

⊢ ∀n m. tri n < tri m ⇔ n < m

⊢ ∀n m. n < m ⇒ tri n < tri m

⊢ (tri n = 0 ⇔ n = 0) ∧ (0 = tri n ⇔ n = 0)

⊢ tri n = n * (n + 1) DIV 2

⊢ n ≤ tri n

⊢ 2 * tri n = n * (n + 1)