The ring of integers adjoined with a square root of d. These have the form a + b √d where a b : ℤ. The components are called re and im by analogy to the negative d case, but of course both parts are real here since d is nonnegative.

Convert an integer to a ℤ√d

The zero of the ring

The one of the ring

The representative of √d in the ring

Addition of elements of ℤ√d

Negation in ℤ√d

Conjugation in ℤ√d. The conjugate of a + b √d is a - b √d.

Multiplication in ℤ√d

Read sq_le a c b d as a √c ≤ b √d

"Generalized" nonneg. nonnegg c d x y means a √c + b √d ≥ 0; we are interested in the case c = 1 but this is more symmetric

Nonnegativity of an element of ℤ√d.

A nonsquare is a natural number that is not equal to the square of an integer. This is implemented as a typeclass because it's a necessary condition for much of the Pell equation theory.