Organize examples with native_decide lint disabled

Summary

Create a dedicated section Examples in each proofs file to contain example assertions that use native_decide without triggering the linter.style.nativeDecide lint that applies to the rest of the codebase.

Approach

Use section with lint option disabled:

• Theorems and core library code remain strict (no native_decide)
• Examples use native_decide for quick verification without linter noise
• Clear signal about code intent and verification guarantees

Files to refactor

• CharCorrectness.lean
• (other proof files as they accumulate examples)

Notes

• Place examples section at end of file
• Examples should be non-library assertions only
• Theorems stay outside this section and use traditional proofs

Inizia con CharCorrectness.lean e controlla come sono organizzate le sue dimostrazioni e i suoi esempi. Esegui il refactoring del file in modo che alla fine compaia una sezione dedicata Examples, con native_decide lint disabilitato al suo interno; mantieni i teoremi e il codice della libreria principale al di fuori di essa. Controlla gli altri file delle dimostrazioni per verificare lo stesso schema man mano che gli esempi aumentano.