feat: Implementing Mutual Fixpoints

[GenericMonkey]

Implementation for issue #46

Ported the fixpointAB and fixpointAB_ne sections from the Rocq implementation.

[GenericMonkey]

Latest commit moves some things around to allow for ported ne proofs to be instances of NonExpansive₂. However, there is some potential clunkiness here, as ContractiveABA and ContractiveABB had to be defined distinctly due to the fact that the associated Proper typeclasses are different in the Rocq version. Namely:

Context {fA_contractive : ∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
Context {fB_contractive : ∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.

There may be a nice way to unify this with the pre-existing Contractive and NonExpansive definitions, but I don't think I have all the intuition to reason about that yet (maybe something like a -c> b -n> b and a -n> b -c> b?)

[GenericMonkey]

Eliminated ContractiveABA and ContractiveABB completely, all results now use (fA : α -c> β -n> α) and (fB : α -c> β -c> β) instead.

If this is undesirable (in the regular fixpoint section it seems that all the results take an (f : α → β) with a separate [Contractive f] instead of passing in an (f : a -c> b), so perhaps there is something I'm missing), please let me know.

[markusdemedeiros]

This is really great work! Your proofs are very clean, a good balance between being terse and being readable.

I pushed some further cleanup and style changes (we try our best to follow the mathlib style guidelines). If you'd like to do so, please feel free to add your name to the authors list at the top of the file.

Re. your comments: I think that using the bundled arrows (-n> and -c>) is fine for now. The jury is still out on whether or not the bundled or unbundled version is best for fixpoints: I've only used it once and had to fill in the contractivity proof by hand anyways, so we should wait and see.

Look over my changes and let me know if you're good to merge!

[GenericMonkey]

Sorry for the delay -- had stepped out for the holidays. Your changes look good, I'm good to merge. Thanks for your help 😀