# Squares in the natural numbers

Content created by Alec Barreto, Egbert Rijke and Fredrik Bakke.

Created on 2023-09-24.

module elementary-number-theory.squares-natural-numbers where

Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.decidable-types
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.negation
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.transport-along-identifications


## Idea

The square n² of a natural number n is the product

  n² := n * n


of n with itself.

## Definition

### Squares of natural numbers

square-ℕ : ℕ → ℕ
square-ℕ n = mul-ℕ n n


### The predicate of being a square of a natural number

is-square-ℕ : ℕ → UU lzero
is-square-ℕ n = Σ ℕ (λ x → n ＝ square-ℕ x)


### The square root of a square natural number

square-root-ℕ : (n : ℕ) → is-square-ℕ n → ℕ
square-root-ℕ _ (root , _) = root


## Properties

### Squares of successors

square-succ-ℕ :
(n : ℕ) →
square-ℕ (succ-ℕ n) ＝ succ-ℕ ((succ-ℕ (succ-ℕ n)) *ℕ n)
square-succ-ℕ n =
( right-successor-law-mul-ℕ (succ-ℕ n) n) ∙
( commutative-add-ℕ (succ-ℕ n) ((succ-ℕ n) *ℕ n))

square-succ-succ-ℕ :
(n : ℕ) →
square-ℕ (succ-ℕ (succ-ℕ n)) ＝ square-ℕ n +ℕ 2 *ℕ n +ℕ 2 *ℕ n +ℕ 4
square-succ-succ-ℕ n =
equational-reasoning
square-ℕ (n +ℕ 2)
＝ (n +ℕ 2) *ℕ n +ℕ (n +ℕ 2) *ℕ 2
by (left-distributive-mul-add-ℕ (n +ℕ 2) n 2)
＝ square-ℕ n +ℕ 2 *ℕ n +ℕ 2 *ℕ (n +ℕ 2)
by
( ap-add-ℕ {(n +ℕ 2) *ℕ n} {(n +ℕ 2) *ℕ 2}
( commutative-mul-ℕ (n +ℕ 2) 2))
＝ square-ℕ n +ℕ 2 *ℕ n +ℕ 2 *ℕ n +ℕ 4
by
( ap-add-ℕ {square-ℕ n +ℕ 2 *ℕ n} {2 *ℕ (n +ℕ 2)}
( refl)


### n > √n for n > 1

The idea is to assume n = m + 2 ≤ sqrt(m + 2) for some m : ℕ and derive a contradiction by squaring both sides of the inequality

greater-than-square-root-ℕ :
(n root : ℕ) → ¬ ((n +ℕ 2 ≤-ℕ root) × (n +ℕ 2 ＝ square-ℕ root))
greater-than-square-root-ℕ n root (pf-leq , pf-eq) =
( square-ℕ root)
( square-ℕ n +ℕ 2 *ℕ n +ℕ n +ℕ 2)
( 0)
( tr
( leq-ℕ (square-ℕ n +ℕ 2 *ℕ n +ℕ n +ℕ 2 +ℕ square-ℕ root))
( concatenate-eq-leq-ℕ
( square-ℕ root)
( inv
( lemma ∙
( ap-add-ℕ {square-ℕ n +ℕ 2 *ℕ n +ℕ n +ℕ 2} {n +ℕ 2}
( refl)
( pf-eq))))
( preserves-leq-mul-ℕ (n +ℕ 2) root (n +ℕ 2) root pf-leq pf-leq)))
where
lemma : square-ℕ (n +ℕ 2) ＝ square-ℕ n +ℕ 2 *ℕ n +ℕ n +ℕ 2 +ℕ n +ℕ 2
lemma =
equational-reasoning
square-ℕ (n +ℕ 2)
＝ square-ℕ n +ℕ 2 *ℕ n +ℕ 2 *ℕ n +ℕ 4
by (square-succ-succ-ℕ n)
＝ square-ℕ n +ℕ 2 *ℕ n +ℕ (n +ℕ 2 +ℕ n +ℕ 2)
by
( ap-add-ℕ {square-ℕ n +ℕ 2 *ℕ n} {2 *ℕ n +ℕ 4}
( refl)
( equational-reasoning
2 *ℕ n +ℕ 4
＝ n +ℕ n +ℕ 2 +ℕ 2
by
( ap-add-ℕ {2 *ℕ n} {4}
( left-two-law-mul-ℕ n)
( refl))
＝ n +ℕ 2 +ℕ 2 +ℕ n
by (commutative-add-ℕ n (n +ℕ 2 +ℕ 2))
＝ n +ℕ 2 +ℕ (2 +ℕ n)
by (associative-add-ℕ (n +ℕ 2) 2 n)
＝ n +ℕ 2 +ℕ (n +ℕ 2)
by
( ap-add-ℕ {n +ℕ 2} {2 +ℕ n}
( refl)
＝ square-ℕ n +ℕ 2 *ℕ n +ℕ n +ℕ 2 +ℕ n +ℕ 2
by
( inv
( square-ℕ n +ℕ 2 *ℕ n)
( n +ℕ 2)
( n +ℕ 2)))


### Squareness in ℕ is decidable

is-decidable-big-root :
(n : ℕ) → is-decidable (Σ ℕ (λ root → (n ≤-ℕ root) × (n ＝ square-ℕ root)))
is-decidable-big-root 0 = inl (0 , star , refl)
is-decidable-big-root 1 = inl (1 , star , refl)
is-decidable-big-root (succ-ℕ (succ-ℕ n)) =
inr (λ H → greater-than-square-root-ℕ n (pr1 H) (pr2 H))

is-decidable-is-square-ℕ : (n : ℕ) → is-decidable (is-square-ℕ n)
is-decidable-is-square-ℕ n =
is-decidable-Σ-ℕ n
( λ x → n ＝ square-ℕ x)
( λ x → has-decidable-equality-ℕ n (square-ℕ x))
( is-decidable-big-root n)