Add O(1) native structural Binomial Theorem for Nat

[alfredoVallejoM]

Description
This PR introduces a completely standalone, structurally inductive proof of Newton's Binomial Theorem over ℕ.

Motivation: Performance & Simplicity
While the standard library already provides generalized binomial expansions via Algebra.CommutativeSemiring, relying on this algebraic hierarchy introduces two significant issues when working strictly with natural numbers:

1. Type-checking Overhead: Utilizing generalized semirings for heavy polynomial expansions in formal verification macros or reflection tactics incurs a massive abstraction penalty during type-checking. By anchoring this specific implementation natively to Data.Nat, this module achieves O(1) unification performance.
2. Simplicity and Ergonomics: When a user is proving properties specific to ℕ, forcing them to navigate, import, and instantiate multiple layers of algebraic abstraction adds unnecessary cognitive load and boilerplate. This standalone proof provides a direct, ergonomic tool for ℕ-specific workflows.

Context: Origin of this Contribution
This module is an abstraction extracted from a larger formal verification project I have been developing. In that context, I encountered severe type-checking overhead and unnecessary complexity when attempting to use the standard library's generalized binomial theorem for heavy proofs. To bypass this bottleneck, I had to develop and prove the theorem natively and strictly for ℕ. I am upstreaming this isolated solution so that others facing similar issues can benefit from its directness.

Changes:

• Added Data.Nat.Binomial.Base for computational definitions.
• Added Data.Nat.Binomial.Properties for propositional equalities.
• Updated EverythingSafe.agda and CHANGELOG.md via the automated build tools.

All code adheres to --cubical-compatible --safe options, standard library naming conventions, and whitespace policies.

---

Methodology & AI Disclosure
In the interest of full transparency regarding the authorship of this contribution:
I identified the type-checking performance bottleneck and the usability issues with the general semiring approach, and I designed the strategy to solve it via native structural induction. However, the entirety of the Agda code, proofs, and structural refactoring were generated using advanced LLMs (AI) through iterative prompt engineering.

My role was architectural oversight, rigorous prompting, and local verification (ensuring it passes make test and complies with all agda-stdlib CI/CD requirements). I am submitting this because I believe the resulting optimization and simplified ergonomics hold significant value for the Agda community.

[MatthewDaggitt]

Thank you for the proposed contribution!

As a rule of thumb, we prefer not to duplicate definitions in the library. To that end, we would much rather see what we could do to optimise the performance of the generalised formulation of the binomial theorem rather than immediately jump to reimplementing a specialised version.

The first step to doing so would be for you to provide us with a minimal example that uses the current version of the binomial version in the library and explain concretely what performance and ergonomic issues you are running into. We can then assess whether we need a solution as heavyweight as this PR.