#
Preliminaries

Let's extend the library on rings and algebraic numbers
with some easy lemmas first.

##
Question -2: prove that if a sum of natural numbers is 1 then one of its term is 0 and the other is 1

Note that we do not consider nat but the copy of nat which is embeded
in the algebraic numbers algC. The theorem already exists for nat, and
we suggest you use a compatibility lemma numbers between nat and Cnat

##
Question -1: The real part of product

##
Question 0: The imaginary part of product

(it's the same, don't do it if takes more than 5s

#
The ring of Gauss integers

- Ref: exercices de mathematiques oraux X-ENS algebre 1
- Exercice 3.10. ENS Lyon

First we define a predicate for the algebraic numbers which are gauss integers.

##
Question 1: Prove that integers are gauss integers

##
Question 2: Prove that gauss integers form a subfield

There follows the boilerplate to use the proof GI_subring in order to
canonically provide a subring structure to the predicate gaussInteger.

Finally, we define the type of Gauss Integer, as a sigma type of
algebraic numbers. We soon prove that this is in fact a sub type.

We make the defining property of GI a Hint

We provide the subtype property.

- This makes it possible to use the generic operator
val

to get an
algC from a Gauss Integer.

We deduce that the real and imaginary parts of a GI are integers

We provide a ring structure to the type GI, using the subring
canonical property for the predicate gaussInteger

- Now we build the unitRing and comUnitRing structure of gauss
integers. Contrarily to the previous structures, the operator is
not the same as on algebraics. Indeed the invertible algebraics are
not necessarily invertible gauss integers.

- Hence, we define the inverse of gauss integers as follow : if the
algebraic inverse happens to be a gauss integer we recover the
proof and package it together with the element and get a gauss
integer, otherwise, we default to the identity.

- A gauss integer is invertible if the algbraic inverse is a gauss
integer.

##
Question 3: prove a few facts in order to find a comUnitRingMixin

for GI, and then instantiate the interfaces of unitRingType and
comUnitRingType.

Do only one of the following proofs.

##
Question 4: Show that gauss integers are stable by conjugation.

We use this fact to build the conjugation of a gauss Integers

We now define the norm (stasm) for gauss integer, we don't need to
specialize it to gauss integer so we define it over algebraic numbers
instead.

##
Question 4: Show that the gaussNorm of x is the square of the complex modulus of x

Hint: only one rewrite with the right theorem.

##
Question 5: Show that the gaussNorm of an gauss integer is a natural number.

##
Question 6: Show that gaussNorm is multiplicative (on all algC).

Hint: use morphism lemmas `rmorph1`

and `rmorphM`

##
Question 7 (hard): Find the invertible elements of GI

- This is question 1 of the CPGE exercice

Do unitGI_norm1 first, and come back to side lemmas later.