Definition of 8-bit addition and local proof

[gio54321]

Issues #5 and #10
It turns out that having the assumption p > 512 is very important for the proof. For now there are explicit field assumptions here, but they will be refactored (possibly as part of #12) in some global structure that takes into account all the global assumptions of the field we are working on.

[gio54321]

The soundness direction of the 8-bit addition is proven, the completeness direction should be easier but IMO before tackling that we should focus on providing a good set of utility theorems/tactics for working with "large enough" fields. Once those are in place we can refactor the proof using those, which should hopefully be also easier to read.
Indeed, most of the soundness proof for the carry=1 case is about proving that if the field is large enough, then the addition of byte values does not wrap around the prime modulus. After that the proof follows easily

[gio54321]

Since those issues are tightly coupled, this PR partially addresses also #12, refactoring some utility theorems over large enough fields.
About the definition of ordering over the field, on a second thought I think it is cleaner to leave the ZMod.val call explicit when defining specs. Suppose we were to define the LT relation as this

instance (p : ℕ) : LT (F p) := ⟨fun x y => x.val < y.val⟩

Then take this expression

variable {x y : F p}
#check (x+y) < 5

The + operation is taken over F p, then the sum is cast to its value and compared with the natural 5. Instead writing explicitly

#check (x.val + y.val) < 5

makes sure that all values are taken as their representation in Nat before doing any operations (which is usually what we want)

[mitschabaude]

This is awesome!!

[mitschabaude]

it's nice how well simp works here on forallList