[PARTIAL] Functional equational approach based on Pace Nielsen's proof

[lyphyser]

I have formalized everything except the case 1 check and constructing the final function based on extensions, but don't have time to finish it, so posting this so someone can maybe finish it.

It's designed to constructively create the counterexample and represents the free abelian group using DFinsupp; it would be nice to cut down on that setup code, but I'm not sure if there is a shorter way of doing it especially constructively.

The partial sets are E are defined as partial functions, again using DFinsupp going to an Option type; the "fup" def lifts them to Option -> Option functions that are none on none.

The construction follows the paper and there are some additional notes on why Case 1 holds, which may help in designing its proof.

[teorth]

I'm inclined to leave this PR unmerged for now until someone reclaims #506, and they can decide to what extent they will build off of this one. (Though one argument in favor of merging now is that it will avoid merge conflicts and build issues later on. So perhaps one can revisit this issue in a few days if nobody ends up reclaiming #506.)

[Shreyas4991]

I'm inclined to leave this PR unmerged for now until someone reclaims #506, and they can decide to what extent they will build off of this one. (Though one argument in favor of merging now is that it will avoid merge conflicts and build issues later on. So perhaps one can revisit this issue in a few days if nobody ends up reclaiming #506.)

In that case I will mark it as a draft PR