More efficient implementation of /, % and GCD

[LorenzoMolena]

The definition of gcd that uses well-founded induction and % from Cubical.Data.Fin has some performance issues.
I also noticed that quotient_/_ and remainder_/_ take quite some time to normalize, so I added alternative implementations, called quotient'_/_ and remainder'_/_, using the built-in helper functions from Agda.Builtin.Nat. Lemmas about these helper functions are adapted from the standard library.

I only proved the necessary properties (≡remainder'+quotient' and mod'<) required to define the efficient version of GCD.
I have already tested whether the performance issues come solely from this, but it seems there are other factors as well, particularly the use of well-founded induction over the naturals.

In this PR, the new proposed implementation becomes the default one, but the previous implementation can still be found at the end of the GCD file, with a prime (') symbol in the name.
The extensional equality between the two implementations is easily proved by the fact that GCD m n is a proposition.

This improvement enables fast fraction reduction and, combined with PR #1245, addresses efficiency for rational arithmetic (#1124)

@felixwellen, please let me know if this new implementation is appropriate.

[felixwellen]

I'm just coming back from vacation and I'll be at a conference next week, so it might take a bit until I can look at it. Generally, I think it is reasonable to use the faster primitives.