fix(specs): auto triggers for Z3 quantifiers

[liamjdavis]

This pull request improves documentation and code clarity around trigger annotations for forall quantifiers in Verus, and updates comments for better readability and consistency. The main focus is on explaining trigger usage, applying explicit trigger annotations to suppress warnings, and making comments more concise.

Documentation improvements:

• Expanded the explanation of trigger annotations for forall quantifiers in CONTRIBUTING.md, detailing the difference between #![auto], #[trigger], and #![trigger ...], and providing practical advice on when to use each.

Trigger annotation updates:

• Added #![auto] trigger annotations to relevant forall statements in verified/src/ingestion_specs.rs to suppress low-confidence trigger warnings and clarify intent in both specifications and proofs. [1] [2] [3]

Comment and style enhancements:

• Updated comments throughout verified/src/ingestion_specs.rs for clarity, conciseness, and consistency, including improving explanations and standardizing formatting in function bodies and assertions. [1] [2] [3] [4]